exists_nat_eq_of_le_nat — Mathlib

English

If c ≤ n for some natural n, then there exists m ≤ n with c = m.

Русский

Если кардинал c ≤ n для некоторого натурального n, то существует m ≤ n такой, что c = m.

LaTeX

$$$ {c : \mathsf{Cardinal}} \ {n : \mathbb{N}} (h : c \le n) : \exists m, m \le n \land c = m$$$

Lean4

theorem exists_nat_eq_of_le_nat {c : Cardinal} {n : ℕ} (h : c ≤ n) : ∃ m, m ≤ n ∧ c = m :=
  by
  lift c to ℕ using h.trans_lt (nat_lt_aleph0 _)
  exact ⟨c, mod_cast h, rfl⟩

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