le_intro — Mathlib

English

If a bound holds for every measurable nonempty set, then μ1 ≤ μ2.

Русский

Если существует граница на значения μ1(S) ≤ μ2(S) для каждого измеримого ненулевого множества, то μ1 ≤ μ2.

LaTeX

$$$ \\left( \\forall S,\\ MeasurableSet(S) \\land S \\neq \\varnothing \\Rightarrow μ_1(S) \\le μ_2(S) \\right) \\Rightarrow μ_1 \\le μ_2 $$$

Lean4

theorem le_intro (h : ∀ s, MeasurableSet s → s.Nonempty → μ₁ s ≤ μ₂ s) : μ₁ ≤ μ₂ :=
  le_iff.2 fun s hs ↦ s.eq_empty_or_nonempty.elim (by rintro rfl; simp) (h s hs)

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