English
A collection B is a basis iff every open set U can be expressed as a union of subfamily of B: there exists Us ⊆ B with U = sSup Us.
Русский
Множество B является базисом тогда и только тогда, когда любое открытое множество U может быть выражено как объединение подсемейки B: существует Us ⊆ B с U = sSup Us.
LaTeX
$$$\operatorname{IsBasis}(B) \iff \forall U \in \operatorname{Opens}(\alpha), \exists Us \subseteq B, U = \bigcup Us$$$
Lean4
theorem isBasis_iff_cover {B : Set (Opens α)} : IsBasis B ↔ ∀ U : Opens α, ∃ Us, Us ⊆ B ∧ U = sSup Us :=
by
constructor
· intro hB U
refine ⟨{V : Opens α | V ∈ B ∧ V ≤ U}, fun U hU => hU.left, ext ?_⟩
rw [coe_sSup, hB.open_eq_sUnion' U.isOpen]
simp_rw [sUnion_eq_biUnion, iUnion, mem_setOf_eq, iSup_and, iSup_image]
rfl
· intro h
rw [isBasis_iff_nbhd]
intro U x hx
rcases h U with ⟨Us, hUs, rfl⟩
rcases mem_sSup.1 hx with ⟨U, Us, xU⟩
exact ⟨U, hUs Us, xU, le_sSup Us⟩
