ofHom_apply — Mathlib

English

Let X and Y be lattices and f: X → Y a lattice hom. Then the function underlying f coincides with f on every element: for all x in X, (ofHom f)(x) = f(x).

Русский

Пусть X и Y — решетки и f: X → Y — гомоморфизм решетки. Тогда базовая функция, лежащая в основе f, отображает x в f(x) для каждого x ∈ X.

LaTeX

$$$ \forall x \in X,\ (\mathrm{ofHom}(f))(x) = f(x). $$$

Lean4

theorem ofHom_apply {X Y : Type u} [Lattice X] [Lattice Y] (f : LatticeHom X Y) (x : X) : (ofHom f) x = f x :=
  rfl

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