English
Applying a lattice homomorphism g after f to a Sublattice L equals applying the composed homomorphism g ∘ f to L: (L.map f).map g = L.map (g ∘ f).
Русский
Применение гомоморфизма g после f к подрешётке L равносильно применению композиции g ∘ f: (L.map f).map g = L.map (g ∘ f).
LaTeX
$$(L.map f).map g = L.map (g.comp f)$$
Lean4
@[simp]
theorem map_map (g : LatticeHom β γ) (f : LatticeHom α β) : (L.map f).map g = L.map (g.comp f) :=
SetLike.coe_injective <| image_image _ _ _