English
Assume α is a semilattice with sup, with decidable ≤ and IsTotal ≤. Then the supremum operation coincides with the default maximum function: ⊔ equals maxDefault.
Русский
Пусть α — полная полукрёстная решётка с верхней гранью, при этом ≤ разрешимо сравнить и порядок тотален. Тогда операция объединения совпадает с функцией maxDefault.
LaTeX
$$$ (\,\sqcup\,) = (\maxDefault : α \to α \to α) $$$
Lean4
theorem sup_eq_maxDefault [SemilatticeSup α] [DecidableLE α] [IsTotal α (· ≤ ·)] : (· ⊔ ·) = (maxDefault : α → α → α) :=
by
ext x y
unfold maxDefault
split_ifs with h'
exacts [sup_of_le_right h', sup_of_le_left <| (total_of (· ≤ ·) x y).resolve_left h']
