inl — Mathlib

English

Compatibility of inclusions across lexicographic product constructions.

Русский

Совместимость вложений между лексикографическими произведениями.

LaTeX

$$$\text{inl}$ совместимо через композицию с другими вложениями.$$

Lean4

/-- Given linearly ordered groups with zero M, N, the natural inclusion ordered homomorphism from
M to `WithZero (Mˣ ×ₗ Nˣ)`, which is the linearly ordered group with zero that can be identified
as their product. -/
@[simps!]
nonrec def inl : α →*₀o WithZero (αˣ ×ₗ βˣ)
    where
  __ := (WithZero.map' (toLexMulEquiv ..).toMonoidHom).comp (inl α β)
  monotone' := by simpa using (WithZero.map'_mono (Prod.Lex.toLex_mono)).comp inl_mono

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