nmul_le_iff — Mathlib

English

a ⨳ b ≤ c if and only if for all a' < a and b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'.

Русский

a ⨳ b ≤ c тогда и только тогда, когда для всех a' < a и b' < b выполняется a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'.

LaTeX

$$$\\forall a,b,c \\in \\mathrm{Ordinal},\\ a \\nabla b \\le c \\iff \\forall a' < a, \\forall b' < b,\\ (a' \\nabla b) \\sharp (a \\nabla b') < (c \\nabla a') \\nabla b'$$$

Lean4

theorem nmul_le_iff : a ⨳ b ≤ c ↔ ∀ a' < a, ∀ b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b' := by rw [← not_iff_not];
  simp [lt_nmul_iff]

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