English
If every element of s is strictly less than every element of t, then the chainHeight of s ∪ t equals the sum of chainHeights of s and t.
Русский
Если каждый элемент s меньше любого элемента t, цепная высота объединения s ∪ t равна сумме цепных высот s и t.
LaTeX
$$(∀ a ∈ s, ∀ b ∈ t, a < b) ⇒ (s ∪ t).chainHeight = s.chainHeight + t.chainHeight$$
Lean4
theorem chainHeight_union_eq (s t : Set α) (H : ∀ a ∈ s, ∀ b ∈ t, a < b) :
(s ∪ t).chainHeight = s.chainHeight + t.chainHeight :=
by
cases h : t.chainHeight
· rw [add_top, eq_top_iff, ← h]
exact Set.chainHeight_mono subset_union_right
apply le_antisymm
· rw [← h]
exact chainHeight_union_le
rw [← add_zero (s ∪ t).chainHeight, ← WithTop.coe_zero, ENat.some_eq_coe, chainHeight_add_le_chainHeight_add]
intro l hl
obtain ⟨l', hl', rfl⟩ := exists_chain_of_le_chainHeight t h.symm.le
refine ⟨l ++ l', ⟨IsChain.append hl.1 hl'.1 fun x hx y hy ↦ ?_, fun i hi ↦ ?_⟩, by simp⟩
· exact H x (hl.2 _ <| mem_of_mem_getLast? hx) y (hl'.2 _ <| mem_of_mem_head? hy)
· rw [mem_append] at hi
rcases hi with hi | hi
exacts [Or.inl (hl.2 _ hi), Or.inr (hl'.2 _ hi)]
