English
IsInjective (Prod.map f g) iff Injective f and Injective g (under Nonempty assumptions).
Русский
Инъективность Prod.map эквивалентна инъективности f и g при некоторых предположениях о непустоте.
LaTeX
$$Iff (Injective (Prod.map f g)) (And (Injective f) (Injective g))$$
Lean4
@[simp]
theorem map_injective [Nonempty α] [Nonempty β] {f : α → γ} {g : β → δ} :
Injective (map f g) ↔ Injective f ∧ Injective g :=
⟨fun h =>
⟨fun a₁ a₂ ha => by
inhabit β
injection @h (a₁, default) (a₂, default) (congr_arg (fun c : γ => Prod.mk c (g default)) ha :), fun b₁ b₂ hb =>
by
inhabit α
injection @h (default, b₁) (default, b₂) (congr_arg (Prod.mk (f default)) hb :)⟩,
fun h => h.1.prodMap h.2⟩
