isSuccLimit_mul_left — Mathlib

English

If l is IsSuccLimit a and b > 0, then a·b is IsSuccLimit.

Русский

Если l — IsSuccLimit a и b > 0, то a·b — IsSuccLimit.

LaTeX

$$$\forall a,b \in \mathrm{Ordinal}, IsSuccLimit(a) \rightarrow 0 < b \rightarrow IsSuccLimit(a \cdot b)$$$

Lean4

theorem isSuccLimit_mul_left {a b : Ordinal} (l : IsSuccLimit a) (b0 : 0 < b) : IsSuccLimit (a * b) :=
  by
  rcases zero_or_succ_or_isSuccLimit b with (rfl | ⟨b, rfl⟩ | lb)
  · exact b0.false.elim
  · rw [mul_succ]
    exact isSuccLimit_add _ l
  · exact isSuccLimit_mul l.bot_lt lb

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