le_iff — Mathlib

English

For measures μ1, μ2, μ1 ≤ μ2 if and only if μ1(s) ≤ μ2(s) for every measurable set s.

Русский

Для мер μ1, μ2 верно: μ1 ≤ μ2 тогда и только тогда, когда μ1(S) ≤ μ2(S) для каждого измеримого множества S.

LaTeX

$$$ μ_1 \\le μ_2 \\iff \\forall S,\\ MeasurableSet(S) \\rightarrow μ_1(S) \\le μ_2(S) $$$

Lean4

theorem le_iff : μ₁ ≤ μ₂ ↔ ∀ s, MeasurableSet s → μ₁ s ≤ μ₂ s :=
  outerMeasure_le_iff

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