eq_nat_of_le_nat — Mathlib

English

If a nimber a is below the natural-number bound b (a ≤* b), then a equals the nimber of some natural number c (a = *c).

Русский

Если Nimber a лежит ниже числового предела b (a ≤* b), то a равен Nimber числа c (a = *c) для некоторого c ∈ ℕ.

LaTeX

$$$a \le^* b \Rightarrow \exists c\in\mathbb{N},\ a = \ast c$$$

Lean4

theorem eq_nat_of_le_nat {a : Nimber} {b : ℕ} (h : a ≤ ∗b) : ∃ c : ℕ, a = ∗c :=
  Ordinal.lt_omega0.1 (h.trans_lt (nat_lt_omega0 b))

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