interior_paramSet — Mathlib

English

The almost-everywhere equivalence between the closure and the interior holds for the paramSet under volume measure.

Русский

ПсевдоэквивалентностьClosure и Interior для paramSet относительно объёма.

LaTeX

$$closure(paramSet K) =ᵐ[volume] interior(paramSet K)$$

Lean4

theorem interior_paramSet : interior (paramSet K) = Set.univ.pi fun w ↦ if w = w₀ then Set.Iio 0 else Set.Ioo 0 1 := by
  simp [interior_pi_set Set.finite_univ, apply_ite]

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