coprod — Mathlib

English

Two continuous linear maps on a product are equal if and only if they have equal compositions with inl and inr.

Русский

Два непрерывных линейных отображения на произведении равны тогда и только тогда, когда их композиции с inl и inr равны.

LaTeX

$$$$ f = g \iff f \circ inl = g \circ inl \;\land\; f \circ inr = g \circ inr $$$$

Lean4

/-- The continuous linear map given by `(x, y) ↦ f₁ x + f₂ y`. -/
@[simps! coe apply]
def coprod (f₁ : M₁ →L[R] M) (f₂ : M₂ →L[R] M) : M₁ × M₂ →L[R] M :=
  ⟨.coprod f₁ f₂, (f₁.cont.comp continuous_fst).add (f₂.cont.comp continuous_snd)⟩

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