comp_apply — Mathlib

English

For bounded lattices X, Y, Z and morphisms f : X → Y, g : Y → Z, the composite satisfies (f ≫ g) x = g (f x) for all x ∈ X.

Русский

Для объектов BddLat X, Y, Z и морфизмов f : X → Y, g : Y → Z композиция удовлетворяет (f ≫ g) x = g (f x) для всех x ∈ X.

LaTeX

$$\\forall {X Y Z : BddOrd} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X), (f ≫ g) x = g (f x)$$

Lean4

theorem comp_apply {X Y Z : BddOrd} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : (f ≫ g) x = g (f x) := by simp

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