map_injective — Mathlib

English

Injectivity of PLift.map f is equivalent to injectivity of f.

Русский

Инъективность отображения PLift.map f эквивалентна инъективности f.

LaTeX

$$$\\forall {\\alpha \\beta} {f : \\alpha \\rightarrow \\beta}, \\operatorname{Injective}(\\mathrm{PLift.map} f) \\Leftrightarrow \\operatorname{Injective}(f)$$$

Lean4

@[simp]
theorem map_injective : Injective (PLift.map f) ↔ Injective f :=
  (Injective.of_comp_iff' _ down_bijective).trans <| up_injective.of_comp_iff _

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