dom_natCast

Mathlib.Data.Nat.PartENat

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

English

For every n, (n : PartENat).Dom holds.

Русский

Для каждого n элемент (n : PartENat) принадлежит области определения.

LaTeX

$$$\\\\forall x \\\\in \\\\mathbb{N}, (x : \\\\mathrm{PartENat}).\\\\Dom$$$

Lean4

@[simp]
theorem dom_natCast (x : ℕ) : (x : PartENat).Dom :=
  trivial

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

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

Разделы

Аффилиация

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