mul_le_iff_of_isSuccLimit — Mathlib

English

If b is a succ-limit ordinal, then a · b ≤ c if and only if a · b′ ≤ c for all b′ < b.

Русский

Если b — предельная ступенька по succ, то a · b ≤ c тогда и только тогда, когда для всех b′ < b выполняется a · b′ ≤ c.

LaTeX

$$$\forall a,b,c \in \mathrm{Ordinal},\ IsSuccLimit(b) \rightarrow (a \cdot b \le c \iff \forall b' < b,\ a \cdot b' \le c)$$$

Lean4

theorem mul_le_iff_of_isSuccLimit {a b c : Ordinal} (h : IsSuccLimit b) : a * b ≤ c ↔ ∀ b' < b, a * b' ≤ c :=
  ⟨fun h _ l => (mul_le_mul_left' l.le _).trans h,
    fun H =>
      -- We use the `induction` tactic in order to change `h`/`H` too.

    le_of_not_gt <| by
      induction a using inductionOn with
      | H α r =>
        induction b using inductionOn with
        | H β s => exact mul_le_of_limit_aux h H⟩

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