inl — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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