exists_nat_gt

Mathlib.Data.ENat.Basic

URI: https://scilib.ai/kg/mathlib#ENat.exists_nat_gt

English

For any n ∈ ENat with n ≠ ⊤, there exists m ∈ ℕ with n < m.

Русский

Для любого n ∈ ENat, n ≠ ⊤, существует m ∈ ℕ такое, что n < m.

LaTeX

$$$\forall {n : ENat}, n \neq \top \to \exists m : \mathbb{N}, n < m$$$

Lean4

protected theorem exists_nat_gt (hn : n ≠ ⊤) : ∃ m : ℕ, n < m :=
  by
  simp_rw [lt_iff_not_ge]
  exact not_forall.mp <| eq_top_iff_forall_ge.2.mt hn

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru