of_isClosed_subset — Mathlib

English

A closed subset of a σ-compact set is σ-compact.

Русский

Замкнутое подмножество σ-компактного множества снова σ-компактно.

LaTeX

$$$ht : IsSigmaCompact t \rightarrow hs : IsClosed s \rightarrow h : s \subset t \rightarrow IsSigmaCompact s$$$

Lean4

/-- A closed subset of a σ-compact set is σ-compact. -/
theorem of_isClosed_subset {s t : Set X} (ht : IsSigmaCompact t) (hs : IsClosed s) (h : s ⊆ t) : IsSigmaCompact s :=
  by
  rcases ht with ⟨K, hcompact, hcov⟩
  refine ⟨(fun n ↦ s ∩ (K n)), fun n ↦ (hcompact n).inter_left hs, ?_⟩
  rw [← inter_iUnion, hcov]
  exact inter_eq_left.mpr h

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