inlLatticeHom — Mathlib

English

The injection inlₗ defines a lattice homomorphism from α to α ⊕ₗ β, preserving both sup and inf.

Русский

Вложение inlₗ задаёт гомоморфизм решетки от α в α ⊕ₗ β, сохраняющий как верхнюю границу, так и нижнюю границу.

LaTeX

$$$\\mathrm{inl}_{\\ell}: \\text{LatticeHom }\\alpha(\\alpha\\oplus_{\\ell}\\beta)$ with $\\mathrm{toFun}=\\mathrm{inl}_{\\ell}$, $\\mathrm{map\\,sup'}=rfl$, $\\mathrm{map\\,inf'}=rfl$$$

Lean4

/-- `Sum.Lex.inlₗ` as a lattice homomorphism. -/
def inlLatticeHom : LatticeHom α (α ⊕ₗ β) where
  toFun := inlₗ
  map_sup' _ _ := rfl
  map_inf' _ _ := rfl

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