diff — Mathlib

English

The difference of a compact set and an open set is compact.

Русский

Разность компактного множества и открытого множества компактна.

LaTeX

$$$IsCompact(s) \rightarrow IsOpen(t) \rightarrow IsCompact(s \setminus t)$$$

Lean4

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

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