get_natCast

Mathlib.Data.Nat.PartENat

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

English

Let x ∈ ℕ. Then get (x : PartENat) (dom_natCast x) = x.

Русский

Пусть x ∈ ℕ. Тогда get (x : PartENat) (dom_natCast x) = x.

LaTeX

$$$\\\\forall x \\\\in \\\\mathbb{N}, \\\\; get (x : \\\\mathrm{PartENat}) (\\\\mathrm{dom\\\\_natCast} x) = x$$$

Lean4

theorem get_natCast {x : ℕ} : get (x : PartENat) (dom_natCast x) = x :=
  get_natCast' _ _

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

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

Разделы

Аффилиация

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