le_generateFrom_iff_subset_isOpen

English

Let g be a collection of subsets of α and t a topology on α. Then t ≤ generateFrom(g) iff every set in g is open in t; equivalently, g ⊆ {s | IsOpen[t] s}.

Русский

Пусть g — семейство подмножеств α, и t — топология на α. Тогда t ≤ generateFrom(g) тогда и только тогда, когда каждоe множество из g открыто в t; эквивалентно, g ⊆ {s | IsOpen[t] s}.

LaTeX

$$$t \\le generateFrom(g) \\quad\\iff\\quad g \\subseteq \\{s\\;|\\; \\IsOpen[t](s)\\}$$$

Lean4

theorem le_generateFrom_iff_subset_isOpen {g : Set (Set α)} {t : TopologicalSpace α} :
    t ≤ generateFrom g ↔ g ⊆ {s | IsOpen[t] s} :=
  ⟨fun ht s hs => ht _ <| .basic s hs, fun hg _s hs =>
    hs.recOn (fun _ h => hg h) isOpen_univ (fun _ _ _ _ => IsOpen.inter) fun _ _ => isOpen_sUnion⟩

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