toLatticeHom — Mathlib

English

The toLatticeHom map acts as the identity on the underlying function: for every f, the function equals f.

Русский

Переопределение toLatticeHom действует как идентичность на базовой функции: для каждого f функция совпадает с f.

LaTeX

$$$\forall f, \bigl( \text{toLatticeHom}(f) \bigr)(a) = f(a) \text{ for all } a.$$$

Lean4

/-- Reinterpret an order homomorphism to a linear order as a `LatticeHom`. -/
def toLatticeHom (f : F) : LatticeHom α β :=
  f

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