map_injective — Mathlib

English

For any f : α → β, the injectivity of ULift.map f is equivalent to the injectivity of f.

Русский

Для любого f : α → β Иньекция ULift.map f эквивалентна инъективности f.

LaTeX

$$$\\operatorname{Injective}(\\mathrm{ULift.map}\,f) \\iff \\operatorname{Injective}(f)$$$

Lean4

@[simp]
theorem map_injective : Injective (ULift.map f : ULift.{u'} α → ULift.{v'} β) ↔ Injective f :=
  (Injective.of_comp_iff' _ down_bijective).trans <| up_injective.of_comp_iff _

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