everywherePosSubset — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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