lt_mul_iff — Mathlib

English

For NatOrdinal a,b,c, one has c < a · b if and only if there exist a'<a, b'<b with c + a'·b' ≤ a'·b + a·b'.

Русский

Для натуральных порядков a,b,c верно: c < a·b тогда и только тогда, когда существуют a'<a и b'<b such that c + a'·b' ≤ a'·b + a·b'.

LaTeX

$$$c < a \cdot b \iff \exists a' < a, \exists b' < b, c + a' \cdot b' \le a' \cdot b + a \cdot b'$$$

Lean4

theorem lt_mul_iff {a b c : NatOrdinal} : c < a * b ↔ ∃ a' < a, ∃ b' < b, c + a' * b' ≤ a' * b + a * b' :=
  Ordinal.lt_nmul_iff

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