withTopWithBot_comp — Mathlib

English

Composition commutes with the Top-Bot extension: (f ∘ g).withTopWithBot = f.withTopWithBot ∘ g.withTopWithBot.

Русский

Композиция сохраняется в расширении Top-Bot: (f ∘ g).withTopWithBot = f.withTopWithBot ∘ g.withTopWithBot.

LaTeX

$$$ (f \\circ g).withTopWithBot = f.withTopWithBot \\circ g.withTopWithBot $$$

Lean4

@[simp]
theorem withTopWithBot_comp (f : LatticeHom β γ) (g : LatticeHom α β) :
    (f.comp g).withTopWithBot = f.withTopWithBot.comp g.withTopWithBot := by ext; simp

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