open_eq_iUnion — Mathlib

English

An open set can be written as a union of basis elements, i.e., as an index-wise union of sets from B.

Русский

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

LaTeX

$$open_eq_iUnion {B : Set (Set α)} (hB : IsTopologicalBasis B) {u : Set α} : IsOpen u ↔ ∃ (β : Type u) (f : β → Set α), (u = ⋃ i, f i) ∧ ∀ i, f i ∈ B$$

Lean4

theorem open_eq_iUnion {B : Set (Set α)} (hB : IsTopologicalBasis B) {u : Set α} (ou : IsOpen u) :
    ∃ (β : Type u) (f : β → Set α), (u = ⋃ i, f i) ∧ ∀ i, f i ∈ B :=
  ⟨↥({s ∈ B | s ⊆ u}), (↑), by
    rw [← sUnion_eq_iUnion]
    apply hB.open_eq_sUnion' ou, fun s => And.left s.2⟩

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