prod_ext_iff — Mathlib

English

The extensionality principle for product maps is encoded as a lemma that splits ext into the two coordinates.

Русский

Принцип экстенсиональности на произведение отображений разлагается на две координаты.

LaTeX

$$$ \\text{prod\_ext} \\{f,g\\} (hl, hr) : f = g \\iff (f.circ inl = g.circ inl) \\land (f.circ inr = g.circ inr) $$$

Lean4

theorem prod_ext_iff {f g : M × M₂ →ₗ[R] M₃} :
    f = g ↔ f.comp (inl _ _ _) = g.comp (inl _ _ _) ∧ f.comp (inr _ _ _) = g.comp (inr _ _ _) :=
  (coprodEquiv ℕ).symm.injective.eq_iff.symm.trans Prod.ext_iff

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