map — Mathlib

English

The image of a Sublattice under a lattice homomorphism is a Sublattice of the codomain.

Русский

Образ подрешетки под гомоморфизмом решётки является подрешеткой кодом.

LaTeX

$$def map (f : LatticeHom α β) (L : Sublattice α) : Sublattice β$$

Lean4

/-- The image of a sublattice along a monoid homomorphism is a sublattice. -/
def map (f : LatticeHom α β) (L : Sublattice α) : Sublattice β
    where
  carrier := f '' L
  supClosed' := L.supClosed.image f
  infClosed' := L.infClosed.image f

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