null_frontier — Mathlib

English

If s is OrdConnected, then the frontier of s has Lebesgue volume zero in the finite product space.

Русский

Если s является OrdConnected, граница frontier s имеет нулевой объём в конечном произведении пространства.

LaTeX

$$$\operatorname{vol}(\partial s)=0$ for s an OrdConnected set in a finite product space.$$

Lean4

theorem null_frontier (hs : s.OrdConnected) : volume (frontier s) = 0 :=
  by
  rw [← hs.upperClosure_inter_lowerClosure]
  exact
    measure_mono_null (frontier_inter_subset _ _) <|
      measure_union_null (measure_inter_null_of_null_left _ (UpperSet.upper _).null_frontier)
        (measure_inter_null_of_null_right _ (LowerSet.lower _).null_frontier)

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