ofHom_apply — Mathlib

English

Let X and Y be bounded distributive lattices and f: X → Y a bounded lattice homomorphism. Then the morphism obtained from f via the constructor ofHom has the same action on elements: (ofHom f)(x) = f(x).

Русский

Пусть X и Y — ограниченные распределительные решётки, а f: X → Y — гомоморфизм решёток. Тогда отображение, полученное из f через конструктор ofHom, действует на элементы так же, как и сам f: (ofHom f)(x) = f(x).

LaTeX

$$$ (\mathrm{ofHom}(f))(x) = f(x) $$$

Lean4

theorem ofHom_apply {X Y : Type u} [DistribLattice X] [BoundedOrder X] [DistribLattice Y] [BoundedOrder Y]
    (f : BoundedLatticeHom X Y) (x : X) : (ofHom f) x = f x :=
  rfl

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