map_injective — Mathlib

English

Sum.map f g is injective if and only if f and g are injective.

Русский

Sum.map f g инъективно тогда и только тогда, когда f и g инъективны.

LaTeX

$$Injective( Sum.map f g ) ⇔ Injective f ∧ Injective g$$

Lean4

@[simp]
theorem map_injective {f : α → γ} {g : β → δ} : Injective (Sum.map f g) ↔ Injective f ∧ Injective g
    where
  mp h := ⟨.of_comp <| h.comp inl_injective, .of_comp <| h.comp inr_injective⟩
  mpr
    | ⟨hf, hg⟩ => hf.sumMap hg

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