inrLatticeHom — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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