fst — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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