coe_comp_lattice_hom' — Mathlib

English

The lattice-homomorphism part of a composed bounded lattice homomorphism equals the composition of the lattice-homomorphism parts.

Русский

Часть, отвечающая за решетку, состава ограниченного гомоморфизма равна композиции частей, отвечающих за решетку.

LaTeX

$$$ (f.comp g : \\mathrm{LatticeHom}(\\alpha, \\gamma)) = (f : \\mathrm{LatticeHom}(\\beta, \\gamma)).comp g $$$

Lean4

@[simp]
  -- `simp`-normal form of `coe_comp_lattice_hom`

theorem coe_comp_lattice_hom' (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) :
    (⟨(f : SupHom β γ).comp g, map_inf (f.comp g)⟩ : LatticeHom α γ) = (f : LatticeHom β γ).comp g :=
  rfl

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