English
LeftInverse of the product map is equivalent to the pair of LeftInverse of the components.
Русский
Левый обратный Prod.map эквивалентен паре левых обратных функций.
LaTeX
$$Iff (Function.LeftInverse (Prod.map f1 g1) (Prod.map f2 g2)) (And (Function.LeftInverse f1 f2) (Function.LeftInverse g1 g2))$$
Lean4
@[simp]
theorem map_leftInverse [Nonempty β] [Nonempty δ] {f₁ : α → β} {g₁ : γ → δ} {f₂ : β → α} {g₂ : δ → γ} :
LeftInverse (map f₁ g₁) (map f₂ g₂) ↔ LeftInverse f₁ f₂ ∧ LeftInverse g₁ g₂ :=
⟨fun h =>
⟨fun b => by
inhabit δ
exact congr_arg Prod.fst (h (b, default)), fun d =>
by
inhabit β
exact congr_arg Prod.snd (h (default, d))⟩,
fun h => h.1.prodMap h.2⟩
