inter_left — Mathlib

English

The intersection of a closed set with a Lindelöf set is Lindelöf.

Русский

Пересечение замкнутого множества с Линдельёфовым множеством есть Линдельёфово.

LaTeX

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

Lean4

/-- The intersection of a closed set and a Lindelöf set is a Lindelöf set. -/
theorem inter_left (ht : IsLindelof t) (hs : IsClosed s) : IsLindelof (s ∩ t) :=
  inter_comm t s ▸ ht.inter_right hs

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