Magnitude conjecture

QuotientSubmoduleEquidistribution.ConvexGeometry.ClosedSets

The lattice of closed sets #

Every closure system is a complete lattice. For a finite anti-exchange closure system, cardinality is a grading: every cover adds exactly one point.

source
@[instance_reducible]
noncomputable instance QuotientSubmoduleEquidistribution.SetClosure.instCompleteLatticeCloseds {E : Type u_1} (c : SetClosure E) :
CompleteLattice (ClosureOperator.Closeds c)

The complete lattice structure transported along the Galois insertion from closed sets to all subsets.

source
def QuotientSubmoduleEquidistribution.SetClosure.pointClosure {E : Type u_1} (c : SetClosure E) (x : E) :
ClosureOperator.Closeds c

A point closure, regarded as an element of the closed-set lattice.

Instances For
    source
    @[simp]
    theorem QuotientSubmoduleEquidistribution.SetClosure.coe_pointClosure {E : Type u_1} (c : SetClosure E) (x : E) :
    ↑(c.pointClosure x) = c {x}
    source
    @[simp]
    theorem QuotientSubmoduleEquidistribution.SetClosure.coe_bot {E : Type u_1} (c : SetClosure E) :
    ↑⊥ = c ∅
    source
    @[simp]
    theorem QuotientSubmoduleEquidistribution.SetClosure.coe_top {E : Type u_1} (c : SetClosure E) :
    ↑⊤ = Set.univ
    source
    @[simp]
    theorem QuotientSubmoduleEquidistribution.SetClosure.coe_inf {E : Type u_1} {c : SetClosure E} (C D : ClosureOperator.Closeds c) :
    ↑(C ⊓ D) = ↑C ∩ ↑D
    source
    @[simp]
    theorem QuotientSubmoduleEquidistribution.SetClosure.coe_sup {E : Type u_1} {c : SetClosure E} (C D : ClosureOperator.Closeds c) :
    ↑(C ⊔ D) = c (↑C ∪ ↑D)
    source
    @[simp]
    theorem QuotientSubmoduleEquidistribution.SetClosure.coe_iSup {E : Type u_1} {c : SetClosure E} {ι : Sort u_2} (f : ι → ClosureOperator.Closeds c) :
    ↑(⨆ (i : ι), f i) = c (⋃ (i : ι), ↑(f i))
    source
    @[simp]
    theorem QuotientSubmoduleEquidistribution.SetClosure.coe_iInf {E : Type u_1} {c : SetClosure E} {ι : Sort u_2} (f : ι → ClosureOperator.Closeds c) :
    ↑(⨅ (i : ι), f i) = ⋂ (i : ι), ↑(f i)
    source
    @[simp]
    theorem QuotientSubmoduleEquidistribution.SetClosure.coe_sSup {E : Type u_1} {c : SetClosure E} (S : Set (ClosureOperator.Closeds c)) :
    ↑(sSup S) = c (⋃ (C : ↑S), ↑↑C)
    source
    theorem QuotientSubmoduleEquidistribution.SetClosure.pointClosure_le_iff {E : Type u_1} {c : SetClosure E} {x : E} {C : ClosureOperator.Closeds c} :
    c.pointClosure x ≤ C ↔ x ∈ ↑C

    A point closure lies below a closed set exactly when the point lies in that set.

    source
    theorem QuotientSubmoduleEquidistribution.SetClosure.pointClosure_injective_closeds {E : Type u_1} {c : SetClosure E} (hae : c.IsAntiExchange) (hempty : c.IsClosed ∅) :
    Function.Injective c.pointClosure

    Distinct ground points give distinct point closures, now as elements of the closed-set lattice.

    source
    theorem QuotientSubmoduleEquidistribution.SetClosure.iSup_pointClosure {E : Type u_1} {c : SetClosure E} (C : ClosureOperator.Closeds c) :
    ⨆ (x : ↑↑C), c.pointClosure ↑x = C

    Every closed set is the supremum of the point closures of its elements.

    source
    theorem QuotientSubmoduleEquidistribution.SetClosure.covBy_eq_insert {E : Type u_1} {c : SetClosure E} [Finite E] (hae : c.IsAntiExchange) {C D : ClosureOperator.Closeds c} (hCD : C ⋖ D) :
    ∃ x ∉ ↑C, ↑D = insert x ↑C

    In a finite anti-exchange closure system, a cover of closed sets adds one point.

    source
    theorem QuotientSubmoduleEquidistribution.SetClosure.ncard_add_one_eq_of_covBy {E : Type u_1} {c : SetClosure E} [Finite E] (hae : c.IsAntiExchange) {C D : ClosureOperator.Closeds c} (hCD : C ⋖ D) :
    (↑C).ncard + 1 = (↑D).ncard

    Cardinality increases by one across every cover.

    source
    @[reducible]
    noncomputable def QuotientSubmoduleEquidistribution.SetClosure.gradeOrder {E : Type u_1} {c : SetClosure E} [Finite E] (hae : c.IsAntiExchange) :
    GradeOrder ℕ (ClosureOperator.Closeds c)

    Cardinality supplies the grading of the finite closed-set lattice.

    Instances For