instFunLike — Mathlib

English

Product operation on continuous affine maps respects evaluation into product spaces: prod f g p = (f p, g p).

Русский

Операция произведения отображений сохраняет вычисление в произведении: prod f g p = (f p, g p).

LaTeX

$$$$\\text{prod}(f,g)(p) = (f(p), g(p)).$$$$

Lean4

@[to_additive]
instance instFunLike : FunLike (A →ₜ* B) A B where
  coe f := f.toFun
  coe_injective' f g
    h := by
    obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f
    obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g
    congr

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