map_rightInverse — Mathlib

English

RightInverse prodMap is equivalent to LeftInverse prodMap (compatibility lemma).

Русский

Правый обратный Prod.map эквивалентен левому обратному через совместимости.

LaTeX

$$RightInverse (Prod.map f1 g1) (Prod.map f2 g2)$$

Lean4

@[simp]
theorem map_rightInverse [Nonempty α] [Nonempty γ] {f₁ : α → β} {g₁ : γ → δ} {f₂ : β → α} {g₂ : δ → γ} :
    RightInverse (map f₁ g₁) (map f₂ g₂) ↔ RightInverse f₁ f₂ ∧ RightInverse g₁ g₂ :=
  map_leftInverse

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