lt_iff' — Mathlib

English

The collection of measures is an ordered additive monoid: addition is monotone in the left argument.

Русский

Меры образуют упорядоченный аддитивный моноид: сложение монотонно по левому аргументу.

LaTeX

$$IsOrderedAddMonoid (Measure α) with the rule: ∀ η, μ ≤ ν ⇒ η + μ ≤ η + ν.$$

Lean4

theorem lt_iff' : μ < ν ↔ μ ≤ ν ∧ ∃ s, μ s < ν s :=
  lt_iff_le_not_ge.trans <| and_congr Iff.rfl <| by simp only [le_iff', not_forall, not_le]

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