injective_toZ — Mathlib

English

For every i0, the map x ↦ toZ i0 x is injective; equal images imply equal inputs.

Русский

Для любого i0 отображение x ↦ toZ_{i0}(x) инъективно; равные значения означают равные аргументы.

LaTeX

$$\\forall x,y,\\; \\operatorname{toZ}_{i_0}(x)=\\operatorname{toZ}_{i_0}(y) \\Rightarrow x=y$$

Lean4

theorem injective_toZ : Function.Injective (toZ i0) := fun _ _ h ↦
  le_antisymm (le_of_toZ_le h.le) (le_of_toZ_le h.symm.le)

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