le_iff' — Mathlib

English

For measures μ1, μ2, μ1 ≤ μ2 if and only if μ1(s) ≤ μ2(s) for all sets s (no measurability assumed).

Русский

Меры μ1, μ2 удовлетворяют μ1 ≤ μ2 тогда и только тогда, когда μ1(S) ≤ μ2(S) для всех множеств S (без предположения измеримости).

LaTeX

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

Lean4

theorem le_iff' : μ₁ ≤ μ₂ ↔ ∀ s, μ₁ s ≤ μ₂ s :=
  .rfl

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