volume_frontier_normLeOne — Mathlib

English

The boundary of normLeOne(K) has volume zero.

Русский

Граница normLeOne(K) имеет нулевой объем.

LaTeX

$$$\\operatorname{vol}(\\operatorname{frontier}(\\operatorname{normLeOne}(K))) = 0$$$

Lean4

theorem volume_frontier_normLeOne : volume (frontier (normLeOne K)) = 0 :=
  by
  rw [frontier, measure_diff, volume_interior_eq_volume_closure, tsub_self]
  · exact interior_subset_closure
  · exact measurableSet_interior.nullMeasurableSet
  · refine lt_top_iff_ne_top.mp <| lt_of_le_of_lt (measure_mono interior_subset) ?_
    rw [volume_normLeOne]
    exact Batteries.compareOfLessAndEq_eq_lt.mp rfl

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