inclusion — Mathlib

English

The inclusion homomorphism from a sublattice L to a bigger sublattice M exists when L ≤ M and is given by inclusion of elements.

Русский

Существует включение подрешетки L в больший L' M, если L ≤ M, и оно задано включением элементов.

LaTeX

$$$ inclusion(h) : LatticeHom L M $ with\\ toFun := Set.inclusion h $$$

Lean4

/-- The inclusion homomorphism from a sublattice `L` to a bigger sublattice `M`. -/
def inclusion (h : L ≤ M) : LatticeHom L M where
  toFun := Set.inclusion h
  map_sup' _ _ := rfl
  map_inf' _ _ := rfl

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