comp_prod_comp_same — Mathlib

English

For order-preserving maps f1,f2: β →o γ and g: α →o β, we have (f1.comp g).prod (f2.comp g) = (f1.prod f2).comp g.

Русский

Для монотонных отображений f1,f2: β →o γ и g: α →o β выполняется тождество (f1.comp g).prod (f2.comp g) = (f1.prod f2).comp g.

LaTeX

$$$ (f_1 \circ g) \mathrm{prod} (f_2 \circ g) = (f_1 \mathrm{prod} f_2) \circ g. $$$

Lean4

theorem comp_prod_comp_same (f₁ f₂ : β →o γ) (g : α →o β) : (f₁.comp g).prod (f₂.comp g) = (f₁.prod f₂).comp g :=
  rfl

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