English
If a is the greatest element of s and b is the greatest element of t in a LinearOrder, then max(a,b) is the greatest element of s ∪ t.
Русский
Если a — наивысший элемент множества s, а b — наивысший элемент множества t в линейном порядке, то max(a,b) — наивысший элемент s ∪ t.
LaTeX
$$$[LinearOrder γ] \; {a b : γ} {s t : Set γ} (ha : IsGreatest s a) (hb : IsGreatest t b) : IsGreatest (s \cup t) (\max a b)$$$
Lean4
/-- If `a` is the greatest element of `s` and `b` is the greatest element of `t`,
then `max a b` is the greatest element of `s ∪ t`. -/
theorem union [LinearOrder γ] {a b : γ} {s t : Set γ} (ha : IsGreatest s a) (hb : IsGreatest t b) :
IsGreatest (s ∪ t) (max a b) :=
⟨by rcases le_total a b with h | h <;> simp [h, ha.1, hb.1], (ha.isLUB.union hb.isLUB).1⟩
