instCharZero — Mathlib

English

PartENat carries a CharZero structure: the canonical map ℕ → PartENat is injective.

Русский

PartENat обладает структурой CharZero: каноническое вложение ℕ в PartENat инъективно.

LaTeX

$$$\\\\forall a,b \\\\in \\\\mathbb{N}, (a : \\\\mathrm{PartENat}) = (b : \\\\mathrm{PartENat}) \\\\Rightarrow a = b$ \\\\; (equivalently) \\\\; (a : \\\\mathrm{PartENat}) = (b : \\\\mathrm{PartENat}) \iff a = b$$$

Lean4

instance : CharZero PartENat where cast_injective := Part.some_injective

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