English
Let f: α → γ and g: β → γ. The map Sum.elim f g: α ⊕ β → γ is injective if and only if f and g are injective and f a ≠ g b for all a, b.
Русский
Пусть f: α → γ и g: β → γ. Отображение Sum.elim f g: α ⊕ β → γ инъективно тогда и только тогда, когда f и g инъективны и ∀ a, b выполняется f a ≠ g b.
LaTeX
$$Injective( Sum.elim f g ) ⇔ Injective f ∧ Injective g ∧ ∀ a b, f a ≠ g b$$
Lean4
@[simp]
theorem elim_injective {γ : Sort*} {f : α → γ} {g : β → γ} :
Injective (Sum.elim f g) ↔ Injective f ∧ Injective g ∧ ∀ a b, f a ≠ g b
where
mp h := ⟨h.comp inl_injective, h.comp inr_injective, fun _ _ => h.ne inl_ne_inr⟩
mpr
| ⟨hf, hg, hfg⟩ => hf.sumElim hg hfg
