isClosed_iff — Mathlib

English

Under the InfPrime assumption on T and OrderGenerates on T, a subset S of T is closed in the relative lower topology if and only if S = hull(T, a) for some a in α.

Русский

При предположении InfPrime на T и OrderGenerates на T множество S ⊆ T замкнуто в относительной нижней топологии тогда и только тогда, когда S = hull(T, a) для некоторого a ∈ α.

LaTeX

$$$IsClosed S \\iff \\exists a, S = \\mathrm{hull}(T, a)$$$

Lean4

theorem isClosed_iff [TopologicalSpace α] [IsLower α] (hT : ∀ p ∈ T, InfPrime p) {S : Set T} :
    IsClosed S ↔ ∃ (a : α), S = hull T a := by simp only [← isOpen_compl_iff, isOpen_iff hT, compl_inj_iff]

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