lindelofSpace_subtype — Mathlib

English

If X is a Hereditarily Lindelöf space, then the subtype { x : X | p x } is Lindelöf for any predicate p.

Русский

Если X — пространство с наследуемой Линдельфовостью, то подтип { x ∈ X | p x } Линдельфово для любого предиката p.

LaTeX

$$[HereditarilyLindelofSpace X] (p : X → Prop) : LindelofSpace { x // p x }$$

Lean4

instance lindelofSpace_subtype [HereditarilyLindelofSpace X] (p : X → Prop) : LindelofSpace { x // p x } :=
  by
  apply isLindelof_iff_LindelofSpace.mp
  exact HereditarilyLindelof_LindelofSets fun x ↦ p x

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