open_eq_sUnion' — Mathlib

English

If u is open, then u equals the union of all basis elements contained in u.

Русский

Если u открыто, то u равняется объединению всех базисных элементов, содержащихся в u.

LaTeX

$$open_eq_sUnion' {B : Set (Set α)} (hB : IsTopologicalBasis B) {u : Set α} (ou : IsOpen u) : u = ⋃₀ {s ∈ B | s ⊆ u}$$

Lean4

/-- Any open set is the union of the basis sets contained in it. -/
theorem open_eq_sUnion' {B : Set (Set α)} (hB : IsTopologicalBasis B) {u : Set α} (ou : IsOpen u) :
    u = ⋃₀ {s ∈ B | s ⊆ u} :=
  ext fun _a =>
    ⟨fun ha =>
      let ⟨b, hb, ab, bu⟩ := hB.exists_subset_of_mem_open ha ou
      ⟨b, ⟨hb, bu⟩, ab⟩,
      fun ⟨_b, ⟨_, bu⟩, ab⟩ => bu ab⟩

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