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