map_injective — Mathlib

English

A short form of injectivity: if map f(x1) = map f(x2) then x1 = x2 (for elements in WithTop).

Русский

Краткая форма инъекции: если map f(x1) = map f(x2), то x1 = x2 (для элементов из WithTop).

LaTeX

$$$\\forall x_1,x_2:\\; \\mathrm{WithTop.map}\\, f\\, x_1 = \\mathrm{WithTop.map}\\, f\\, x_2 \\Rightarrow x_1 = x_2$$$

Lean4

theorem map_injective {f : α → β} (Hf : Injective f) : Injective (WithTop.map f) :=
  Option.map_injective Hf

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