English
Assume α is a topological space and IsLower, with the InfPrime condition on T. A subset S of T is open in the relative lower topology if and only if there exists a ∈ α such that S is the complement of hull(T, a) (restricted to T).
Русский
Пусть α — топологическое пространство и IsLower, с условием InfPrime на T. Подмножество S ⊆ T открыто в относительной нижней топологии тогда и только тогда, когда существует a ∈ α такое, что S является дополнением hull(T, a) (ограниченным до T).
LaTeX
$$$IsOpen S \\iff \\exists a, S = (hull(T, a))^{c}$$$
Lean4
theorem isOpen_iff [TopologicalSpace α] [IsLower α] (hT : ∀ p ∈ T, InfPrime p) (S : Set T) :
IsOpen S ↔ ∃ (a : α), S = (hull T a)ᶜ := by
constructor <;> intro h
· let R := {a : α | (hull T a)ᶜ ⊆ S}
use sSup R
rw [IsTopologicalBasis.open_eq_sUnion' (isTopologicalBasis_relativeLower hT) h]
aesop
· obtain ⟨a, ha⟩ := h
exact
⟨(Ici a)ᶜ, isClosed_Ici.isOpen_compl, ha.symm⟩
/- When `α` is complete, a set is closed in the relative lower topology if and only if it is of the
form `hull T a` for some `a` in `α`.-/
