eq_of_le_of_measure_univ_eq — Mathlib

English

Let μ ≤ ν and μ(univ) = ν(univ). Then μ = ν (under finiteness assumptions on μ).

Русский

Пусть μ ≤ ν и μ(универсум) = ν(универсум). Тогда μ = ν (при допущении конечности μ).

LaTeX

$$$(\mu \le \nu) \land (\mu(\mathrm{univ}) = \nu(\mathrm{univ})) \Rightarrow \mu = \nu$$$

Lean4

theorem eq_of_le_of_measure_univ_eq [IsFiniteMeasure μ] (hμν : μ ≤ ν) (h_univ : μ univ = ν univ) : μ = ν :=
  by
  refine le_antisymm hμν (le_intro fun s hs _ ↦ ?_)
  by_contra! h_lt
  have h_disj : Disjoint s sᶜ := disjoint_compl_right_iff_subset.mpr subset_rfl
  rw [← union_compl_self s, measure_union h_disj hs.compl, measure_union h_disj hs.compl] at h_univ
  exact ENNReal.add_lt_add_of_lt_of_le (measure_ne_top _ _) h_lt (hμν sᶜ) |>.not_ge h_univ.symm.le

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