gc — Mathlib · SciLib

English

There is a Galois connection between the closure operator and the coercion to sets: closure s ≤ t iff s ⊆ t.

Русский

Существует связь Галуа между оператором замыкания и включением: closure s ≤ t тогда и только тогда, когда s ⊆ t.

LaTeX

$$$\\text{gc} : GaloisConnection Closeds.closure ((↑) : Closeds α → Set α)$ with $\,\\forall s: Set α, t: Closeds α,\\; Closeds.closure(s) \\le t \\,\\Leftrightarrow\\; s \\subseteq t$$$

Lean4

theorem gc : GaloisConnection Closeds.closure ((↑) : Closeds α → Set α) := fun _ U =>
  ⟨subset_closure.trans, fun h => closure_minimal h U.isClosed⟩

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