toHereditarilyLindelof — Mathlib

English

A second-countable space is hereditarily Lindelöf; in particular every open subset is Lindelöf.

Русский

Первая счётность пространства приводит к наследуемой Линдельфовости; каждый открытый подмножество Линдельфово.

LaTeX

$$$[SecondCountableTopology X] \\Rightarrow [HereditarilyLindelofSpace X].$$$

Lean4

instance (priority := 100) toHereditarilyLindelof [SecondCountableTopology X] : HereditarilyLindelofSpace X where
  isHereditarilyLindelof_univ t _
    _ := by
    apply isLindelof_iff_countable_subcover.mpr
    intro ι U hι hcover
    have := @isOpen_iUnion_countable X _ _ ι U hι
    rcases this with ⟨t, ⟨htc, htu⟩⟩
    use t, htc
    exact subset_of_subset_of_eq hcover (id htu.symm)

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