open_eq_sUnion — Mathlib

English

An open set is the union of a subcollection of basis elements contained in it.

Русский

Открытое множество является объединением подмножества базисных элементов, содержащихся внутри него.

LaTeX

$$open_eq_sUnion {B : Set (Set α)} (hB : IsTopologicalBasis B) {u : Set α} : IsOpen u ↔ ∃ S ⊆ B, u = ⋃₀ S$$

Lean4

theorem open_eq_sUnion {B : Set (Set α)} (hB : IsTopologicalBasis B) {u : Set α} (ou : IsOpen u) : ∃ S ⊆ B, u = ⋃₀ S :=
  ⟨{s ∈ B | s ⊆ u}, fun _ h => h.1, hB.open_eq_sUnion' ou⟩

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