ofHom_comp — Mathlib

English

Two morphisms between finite bounded distributive lattices are equal if they agree on every element.

Русский

Два морфизма между конечными ограниченными дизъюнктными решетками равны, если они совпадают на каждом элементе.

LaTeX

$$theorem ext {X Y : FinBddDistLat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g$$

Lean4

@[simp]
theorem ofHom_comp {X Y Z : Type u} [PartialOrder X] [BoundedOrder X] [PartialOrder Y] [BoundedOrder Y] [PartialOrder Z]
    [BoundedOrder Z] (f : BoundedOrderHom X Y) (g : BoundedOrderHom Y Z) : ofHom (g.comp f) = ofHom f ≫ ofHom g :=
  rfl

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