snd — Mathlib

English

The continuous homomorphism given by projecting onto the second factor is the map (A × B) → B.

Русский

Непрерывный гомоморфизм проекции на вторую компоненту: (A × B) → B.

LaTeX

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

Lean4

/-- The continuous homomorphism given by projection onto the second factor. -/
@[to_additive (attr := simps!) /-- The continuous homomorphism given by projection onto the second factor. -/
    ]
def snd : (A × B) →ₜ* B :=
  ⟨MonoidHom.snd A B, continuous_snd⟩

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