coframeMinimalAxioms — Mathlib

English

Closed sets satisfy the minimal axioms for a Coframe: a chosen infimum–supremum relation is compatible with their lattice structure in a precise way.

Русский

Замкнутые множества удовлетворяют минимальным аксиомам Coframe: взаимосвязь между Inf и Sup согласуется с их решетчатой структурой в точной форме.

LaTeX

$$$\text{coframeMinimalAxioms} : \mathrm{Coframe.MinimalAxioms}(\mathrm{Closeds}(\alpha)).$$$

Lean4

/-- Closed sets in a topological space form a coframe. -/
def coframeMinimalAxioms : Coframe.MinimalAxioms (Closeds α) where
  iInf_sup_le_sup_sInf a
    s := (SetLike.coe_injective <| by simp only [coe_sup, coe_iInf, coe_sInf, Set.union_iInter₂]).le

Похожие утверждения