map_map — Mathlib

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 _ _ _

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