inr — Mathlib

English

The continuous homomorphism given by including the second factor into the product is x ↦ (1, x).

Русский

Непрерывный гомоморфизм включения второй компоненты в произведение: x ↦ (1, x).

LaTeX

$$$inr: B \\to_* (A \\times B)$$$

Lean4

/-- The continuous homomorphism given by inclusion of the second factor. -/
@[to_additive (attr := simps!) /-- The continuous homomorphism given by inclusion of the second factor. -/
    ]
def inr : B →ₜ* (A × B) :=
  prod 1 (id B)

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