everywherePosSubset — Mathlib

English

If s is compact, then μ.everywherePosSubset s is compact.

Русский

Если s компактно, то μ.everywherePosSubset s компактно.

LaTeX

$$$$ \\text{If } s\\text{ is compact, then } μ.everywherePosSubset s \\text{ is compact.} $$$$

Lean4

protected theorem _root_.IsCompact.everywherePosSubset (hs : IsCompact s) : IsCompact (μ.everywherePosSubset s) :=
  by
  rcases exists_isOpen_everywherePosSubset_eq_diff μ s with ⟨u, u_open, hu⟩
  rw [hu]
  exact hs.diff u_open

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