of_isClosed_subset — Mathlib

English

A closed subset of a compact set is compact.

Русский

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

LaTeX

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

Lean4

/-- A closed subset of a compact set is a compact set. -/
theorem of_isClosed_subset (hs : IsCompact s) (ht : IsClosed t) (h : t ⊆ s) : IsCompact t :=
  inter_eq_self_of_subset_right h ▸ hs.inter_right ht

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