inter_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- The intersection of a Lindelöf set and a closed set is a Lindelöf set. -/
theorem inter_right (hs : IsLindelof s) (ht : IsClosed t) : IsLindelof (s ∩ t) :=
  by
  intro f hnf _ hstf
  rw [← inf_principal, le_inf_iff] at hstf
  obtain ⟨x, hsx, hx⟩ : ∃ x ∈ s, ClusterPt x f := hs hstf.1
  have hxt : x ∈ t := ht.mem_of_nhdsWithin_neBot <| hx.mono hstf.2
  exact ⟨x, ⟨hsx, hxt⟩, hx⟩

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