subtype — Mathlib

English

There exists a canonical lattice hom from L to α given by sending each element of L to its underlying α-value.

Русский

Существует канонический гомоморфизм от L к α, отображающий элемент подрешетки в соответствующее значение α.

LaTeX

$$$ \\text{subtype}(L) : LatticeHom L α $ with \\ toFun := (\\uparrow) $$

Lean4

/-- The natural lattice hom from a sublattice to the original lattice. -/
def subtype (L : Sublattice α) : LatticeHom L α
    where
  toFun := ((↑) : L → α)
  map_sup' _ _ := rfl
  map_inf' _ _ := rfl

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