inter_right — Mathlib

English

If s is compact and t is closed, then their intersection s ∩ t is compact.

Русский

Если s компактно, а t замкнуто, то их пересечение s ∩ t компактно.

LaTeX

$$$IsCompact(s) \rightarrow IsClosed(t) \rightarrow IsCompact(s \cap t)$$$

Lean4

/-- The intersection of a compact set and a closed set is a compact set. -/
theorem inter_right (hs : IsCompact s) (ht : IsClosed t) : IsCompact (s ∩ t) :=
  by
  intro f hnf hstf
  obtain ⟨x, hsx, hx⟩ : ∃ x ∈ s, ClusterPt x f := hs (le_trans hstf (le_principal_iff.2 inter_subset_left))
  have : x ∈ t := ht.mem_of_nhdsWithin_neBot <| hx.mono <| le_trans hstf (le_principal_iff.2 inter_subset_right)
  exact ⟨x, ⟨hsx, this⟩, hx⟩

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