not_isMax_natCast

Mathlib.Data.Nat.PartENat

URI: https://scilib.ai/kg/mathlib#PartENat.not_isMax_natCast

English

For any n ∈ ℕ, (n : PartENat) is not a maximal element.

Русский

Для любого n ∈ ℕ элемент n, приведённый к PartENat, не является максимальным.

LaTeX

$$$ \forall n \in \mathbb{N}, \neg \mathrm{IsMax}(n : \mathrm{PartENat}) $$$

Lean4

theorem not_isMax_natCast (x : ℕ) : ¬IsMax (x : PartENat) :=
  not_isMax_of_lt (natCast_lt_top x)

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

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

Разделы

Аффилиация

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