null_frontier_inter — Mathlib

English

If frontier(s) and frontier(s') both have zero measure, then frontier(s ∩ s') has zero measure.

Русский

Если frontier(s) и frontier(s') имеют нулевую меру, то frontier(s ∩ s') тоже имеет нулевую меру.

LaTeX

$$$\\mu(\\operatorname{frontier}(s \\cap s')) = 0$ при $\\mu(\\operatorname{frontier}(s)) = 0$ и $\\mu(\\operatorname{frontier}(s')) = 0$.$$

Lean4

theorem null_frontier_inter {μ : Measure α'} {s s' : Set α'} (h : μ (frontier s) = 0) (h' : μ (frontier s') = 0) :
    μ (frontier (s ∩ s')) = 0 := by
  apply bot_unique
  calc
    μ (frontier (s ∩ s'))
    _ ≤ μ (frontier s ∪ frontier s') := (measure_mono <| (frontier_inter_subset _ _).trans (by grind))
    _ ≤ μ (frontier s) + μ (frontier s') := (measure_union_le _ _)
    _ = 0 := by simp [h, h']

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