Lax Lean Archive

The closure of intersections and unions

Lax871432.IntersectionsUnions · concepts/Lax871432/IntersectionsUnions.lean · lax-871432

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Lemma

    Let II be an arbitrary index set and let (Fi)i∈I(\mathcal{F}_i)_{i \in I} be a family of graph classes. Then

    cl(⋂i∈IFi)⊆⋂i∈Icl(Fi)and⋃i∈Icl(Fi)⊆cl(⋃i∈IFi).\mathrm{cl}\Big(\bigcap_{i \in I} \mathcal{F}_i\Big) \subseteq \bigcap_{i \in I} \mathrm{cl}(\mathcal{F}_i) \quad \text{and} \quad \bigcup_{i \in I} \mathrm{cl}(\mathcal{F}_i) \subseteq \mathrm{cl}\Big(\bigcup_{i \in I} \mathcal{F}_i\Big).
    Concept map
    6 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 cl_iInf_le_iInf_cl proven

    2 iSup_cl_le_cl_iSup proven

    In the paper

    • page 3 of this submission's paper

    Lean source view on GitHub

    1import Lax871432.DistinguishingClosure
    2
    3/-!
    4---
    5title: The closure of intersections and unions
    6type: lemma
    7---
    8Let II be an arbitrary index set and let (Fi)i∈I(\mathcal{F}_i)_{i \in I} be a family of graph
    9classes. Then
    10cl(⋂i∈IFi)⊆⋂i∈Icl(Fi)and⋃i∈Icl(Fi)⊆cl(⋃i∈IFi).\mathrm{cl}\Big(\bigcap_{i \in I} \mathcal{F}_i\Big) \subseteq \bigcap_{i \in I} \mathrm{cl}(\mathcal{F}_i) \quad \text{and} \quad \bigcup_{i \in I} \mathrm{cl}(\mathcal{F}_i) \subseteq \mathrm{cl}\Big(\bigcup_{i \in I} \mathcal{F}_i\Big).
    11
    12
    13
    14-/
    15
    16open Lax871432.DistinguishingClosure Lax871432.GraphClasses
    17
    18namespace Lax871432.IntersectionsUnions
    19
    20/-- The closure of an intersection is contained in the intersection of the closures. -/
    21axiom cl_iInf_le_iInf_cl {I : Type*} (𝓕 : I → GraphClass) :
    22 cl (⨅ i, 𝓕 i) ≤ ⨅ i, cl (𝓕 i)
    23
    24/-- The union of the closures is contained in the closure of the union. -/
    25axiom iSup_cl_le_cl_iSup {I : Type*} (𝓕 : I → GraphClass) :
    26 ⨆ i, cl (𝓕 i) ≤ cl (⨆ i, 𝓕 i)
    27
    28end Lax871432.IntersectionsUnions
    29
    Show ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…