mul_le_nmul — Mathlib

English

For ordinals a,b, a · b ≤ a ⊗ b.

Русский

Для ординалов a,b верно a·b ≤ a ⊗ b.

LaTeX

$$$a \cdot b \le a \otimes b$$$

Lean4

theorem mul_le_nmul (a b : Ordinal.{u}) : a * b ≤ a ⨳ b :=
  by
  refine b.limitRecOn ?_ ?_ ?_
  · simp
  · intro c h
    rw [mul_succ, nmul_succ]
    exact (add_le_nadd _ a).trans (nadd_le_nadd_right h a)
  · intro c hc H
    rcases eq_zero_or_pos a with (rfl | ha)
    · simp
    · rw [(isNormal_mul_right ha).apply_of_isSuccLimit hc, Ordinal.iSup_le_iff]
      rintro ⟨i, hi⟩
      exact (H i hi).trans (nmul_le_nmul_left hi.le a)

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