English
An order-homomorphism from a linear order to a lattice is a lattice-homomorphism; it preserves sup and inf.
Русский
Гомоморфизм порядка между линейным порядком и решёткой является гомоморфизмом решётки: сохраняет sup и inf.
LaTeX
$$$f(\max(a,b)) = \max(f(a),f(b))$ and $f(\min(a,b)) = \min(f(a),f(b))$; in particular, $f(a\vee b)=f(a)\vee f(b)$ and $f(a\wedge b)=f(a)\wedge f(b)$.$$
Lean4
/-- An order homomorphism from a linear order is a lattice homomorphism. -/
instance (priority := 100) toLatticeHomClass : LatticeHomClass F α β :=
{
‹OrderHomClass F α
β› with
map_sup := fun f a b => by
obtain h | h := le_total a b
· rw [sup_eq_right.2 h, sup_eq_right.2 (OrderHomClass.mono f h : f a ≤ f b)]
· rw [sup_eq_left.2 h, sup_eq_left.2 (OrderHomClass.mono f h : f b ≤ f a)]
map_inf := fun f a b => by
obtain h | h := le_total a b
· rw [inf_eq_left.2 h, inf_eq_left.2 (OrderHomClass.mono f h : f a ≤ f b)]
· rw [inf_eq_right.2 h, inf_eq_right.2 (OrderHomClass.mono f h : f b ≤ f a)] }
