diff — Mathlib

English

The difference of a Lindelöf set with an open set is Lindelöf.

Русский

Разность Линдельёфова множества и открытого множества остается Линдельёфовой.

LaTeX

$$$$\text{IsLindelof}(s) \land \text{IsOpen}(t) \Rightarrow \text{IsLindelof}(s \setminus t).$$$$

Lean4

/-- The set difference of a Lindelöf set and an open set is a Lindelöf set. -/
theorem diff (hs : IsLindelof s) (ht : IsOpen t) : IsLindelof (s \ t) :=
  hs.inter_right (isClosed_compl_iff.mpr ht)

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