get_natCast'

Mathlib.Data.Nat.PartENat

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

English

For any x ∈ ℕ and Dom witness h, get (x : PartENat) h = x.

Русский

Для любого x ∈ ℕ и доказательства Dom, get (x : PartENat) h = x.

LaTeX

$$@[simp, oct] get_natCast' (x : ℕ) (h : (x : PartENat).Dom) : get (x : PartENat) h = x$$

Lean4

@[simp, norm_cast]
theorem get_natCast' (x : ℕ) (h : (x : PartENat).Dom) : get (x : PartENat) h = x := by rw [← natCast_inj, natCast_get]

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

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

Разделы

Аффилиация

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