English
For two well-founded, nonempty sets s and t in a linear order, the minimum of their union is the minimum of their individual minimums.
Русский
Для двух хорошо основанных непустых множеств s и t в линейном порядке минимум их объединения равен минимума минимальных элементов каждого из них.
LaTeX
$$$(hs.unions ht).min (union_nonempty.2 (Or.intro_left _ hsn)) = Min.min (hs.min hsn) (ht.min htn)$$
Lean4
theorem min_union (hs : s.IsWF) (hsn : s.Nonempty) (ht : t.IsWF) (htn : t.Nonempty) :
(hs.union ht).min (union_nonempty.2 (Or.intro_left _ hsn)) = Min.min (hs.min hsn) (ht.min htn) :=
by
refine
le_antisymm (le_min (IsWF.min_le_min_of_subset subset_union_left) (IsWF.min_le_min_of_subset subset_union_right)) ?_
rw [min_le_iff]
exact ((mem_union _ _ _).1 ((hs.union ht).min_mem (union_nonempty.2 (.inl hsn)))).imp (hs.min_le _) (ht.min_le _)
