English
Let p: X → Prop and s ⊆ { x ∈ X | p(x) }. Then s is Lindelöf as a subset of the subtype { x // p x } if and only if its image under the inclusion map into X is Lindelöf in X; i.e. IsLindelof(s) ⇔ IsLindelof(↑''s).
Русский
Пусть p: X → Prop и s ⊆ { x ∈ X | p(x) }. Тогда s является Линдельфовским подмножством в подпространстве { x // p x } тогда и только тогда, когда его образ в X по включению является Линдельфовым в X; то есть IsLindelof(s) ⇔ IsLindelof(↑''s).
LaTeX
$$$\\operatorname{IsLindelof}(s) \\iff \\operatorname{IsLindelof}(\\uparrow''s) \\quad(\\uparrow:\\{x\\;\\mid\\;p(x)\\}\\to X).$$$
Lean4
/-- Sets of subtype are Lindelöf iff the image under a coercion is. -/
theorem isLindelof_iff {p : X → Prop} {s : Set { x // p x }} : IsLindelof s ↔ IsLindelof ((↑) '' s : Set X) :=
IsEmbedding.subtypeVal.isLindelof_iff
