of_isClosed_subset — Mathlib

English

A closed subset of a Lindelöf set is Lindelöf.

Русский

Замкнутое подмножество Линдельёфова множества — Линдельёфово.

LaTeX

$$$$\text{IsLindelof}(s) \land \text{IsClosed}(t) \land t \subseteq s \Rightarrow \text{IsLindelof}(t).$$$$

Lean4

/-- A closed subset of a Lindelöf set is a Lindelöf set. -/
theorem of_isClosed_subset (hs : IsLindelof s) (ht : IsClosed t) (h : t ⊆ s) : IsLindelof t :=
  inter_eq_self_of_subset_right h ▸ hs.inter_right ht

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