le_iff' — Mathlib

English

A second form: v ≤ w if and only if ∀ i, v i ≤ w i (no measurability assumed).

Русский

Вторая форма: v ≤ w тогда и только тогда, когда ∀ i, v i ≤ w i (без предположения о измеримости).

LaTeX

$$$ v \\le w \\iff \\forall i, v(i) \\le w(i) $$$

Lean4

theorem le_iff' : v ≤ w ↔ ∀ i, v i ≤ w i :=
  by
  refine ⟨fun h i => ?_, fun h i _ => h i⟩
  by_cases hi : MeasurableSet i
  · exact h i hi
  · rw [v.not_measurable hi, w.not_measurable hi]

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