natCast_inj

Mathlib.Data.Nat.PartENat

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

English

Nat cast from ℕ to PartENat is injective: (x : PartENat) = y ↔ x = y.

Русский

Каст ℕ в PartENat инъективен: (x : PartENat) = y ⇔ x = y.

LaTeX

$$$\\\\forall x,y \\\\in \\\\mathbb{N}, (x : \\\\mathrm{PartENat}) = y \\\\iff x = y$$$

Lean4

/-- Alias of `Nat.cast_inj` specialized to `PartENat` -/
theorem natCast_inj {x y : ℕ} : (x : PartENat) = y ↔ x = y :=
  Nat.cast_inj

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

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

Разделы

Аффилиация

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