map_natCast_inj — Mathlib

English

Equality of mapped values is equivalent to equality of original ENat arguments: ENat.map Nat.cast m = ENat.map Nat.cast n iff m = n.

Русский

Равенство отображений равно равенству исходников: ENat.map Nat.cast m = ENat.map Nat.cast n эквивалентно m = n.

LaTeX

$$$$ \\mathrm{ENat.map}(\\mathrm{Nat.cast})\,m = \\mathrm{ENat.map}(\\mathrm{Nat.cast})\,n \\iff m = n $$$$

Lean4

@[simp]
theorem map_natCast_inj : m.map (Nat.cast : ℕ → α) = n.map Nat.cast ↔ m = n :=
  map_natCast_injective.eq_iff

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