English
The chainHeight of the union s ∪ t is bounded above by the sum of chainHeights of s and t.
Русский
Цепная высота объединения spr s ∪ t ограничена суммой цепных высот s и t.
LaTeX
$$(s ∪ t).chainHeight ≤ s.chainHeight + t.chainHeight$$
Lean4
theorem chainHeight_union_le : (s ∪ t).chainHeight ≤ s.chainHeight + t.chainHeight := by
classical
refine iSup₂_le fun l hl ↦ ?_
let l₁ := l.filter (· ∈ s)
let l₂ := l.filter (· ∈ t)
have hl₁ : ↑l₁.length ≤ s.chainHeight :=
by
apply Set.length_le_chainHeight_of_mem_subchain
exact ⟨hl.1.sublist filter_sublist, fun i h ↦ by simpa using (of_mem_filter h :)⟩
have hl₂ : ↑l₂.length ≤ t.chainHeight :=
by
apply Set.length_le_chainHeight_of_mem_subchain
exact ⟨hl.1.sublist filter_sublist, fun i h ↦ by simpa using (of_mem_filter h :)⟩
grw [← hl₁, ← hl₂]
simp_rw [l₁, l₂, ← Nat.cast_add, ← Multiset.coe_card, ← Multiset.card_add, ← Multiset.filter_coe]
rw [Multiset.filter_add_filter, Multiset.filter_eq_self.mpr, Multiset.card_add, Nat.cast_add]
exacts [le_add_right rfl.le, hl.2]
