fst — Mathlib

English

The composition of fst with inl is the identity on α.

Русский

Составление fst и inl даёт тождество на α.

LaTeX

$$$(fst\;\_\_).(inl) = id$ на α.$$

Lean4

/-- Given linearly ordered groups with zero M, N, the natural projection ordered homomorphism from
`WithZero (Mˣ ×ₗ Nˣ)` to M, which is the linearly ordered group with zero that can be identified
as their product. -/
@[simps!]
nonrec def fst : WithZero (αˣ ×ₗ βˣ) →*₀o α
    where
  __ := (fst α β).comp (WithZero.map' (toLexMulEquiv ..).symm.toMonoidHom)
  monotone' := by
    -- this can't rely on `Monotone.comp` since `ofLex` is not monotone

    intro x y
    cases x <;> cases y
    · simp
    · simp
    · simp
    · simpa using Prod.Lex.monotone_fst _ _

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