isLindelof_iff_isLindelof_univ — Mathlib

English

For a subset s ⊆ X, IsLindelof s holds if and only if IsLindelof(univ : Set s), i.e., the subspace s is Lindelöf iff its universe (as a subspace) is Lindelöf.

Русский

Для подмножества s ⊆ X справедливо: IsLindelof s тогда же, когда IsLindelof(univ : Set s), то есть подпространство s Линдельфово тогда и только тогда, когда его вселенная как подпространство Линдельфова.

LaTeX

$$$\\operatorname{IsLindelof}(s) \\iff \\operatorname{IsLindelof}(\\operatorname{univ}:\\Set s).$$$

Lean4

theorem isLindelof_iff_isLindelof_univ : IsLindelof s ↔ IsLindelof (univ : Set s) := by
  rw [Subtype.isLindelof_iff, image_univ, Subtype.range_coe]

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