toMeasure_top — Mathlib

English

μ < ν iff μ ≤ ν and there exists a measurable s with μ(s) < ν(s).

Русский

μ < ν тогда и только тогда, когда μ ≤ ν и существует измеримое множество s такое, что μ(s) < ν(s).

LaTeX

$$$ μ < ν \\iff μ ≤ ν ∧ ∃ S, MeasurableSet(S) ∧ μ(S) < ν(S) $$$

Lean4

@[simp]
theorem _root_.MeasureTheory.OuterMeasure.toMeasure_top :
    (⊤ : OuterMeasure α).toMeasure (by rw [OuterMeasure.top_caratheodory]; exact le_top) = (⊤ : Measure α) :=
  toOuterMeasure_toMeasure (μ := ⊤)

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