prodMap — Mathlib

English

If f1,f2 are left-inverse and g1,g2 are left-inverse, then Prod.map f1 g1 and Prod.map f2 g2 are left-inverse.

Русский

Если f1,f2 и g1,g2 имеют свойства левых обратных, то Prod.map f1 g1 и Prod.map f2 g2 образуют левую инверсную пару.

LaTeX

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

Lean4

theorem prodMap (hf : LeftInverse f₁ f₂) (hg : LeftInverse g₁ g₂) : LeftInverse (map f₁ g₁) (map f₂ g₂) := fun a ↦ by
  rw [Prod.map_map, hf.comp_eq_id, hg.comp_eq_id, map_id, id]

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