English
For sets s ⊆ α and t ⊆ β and natural numbers n,m, s.chainHeight + n ≤ t.chainHeight + m if and only if every chain l in s.subchain has a corresponding chain l' in t.subchain with length(l) + n ≤ length(l') + m.
Русский
Для множеств s ⊆ α и t ⊆ β и натур. чисел n,m выполняется: chainHeight(s) + n ≤ chainHeight(t) + m тогда для каждой цепи l ∈ s.subchain существует цепь l' ∈ t.subchain с length(l) + n ≤ length(l') + m.
LaTeX
$$$ s.chainHeight + n \\le t.chainHeight + m \\iff \\forall l \\in s.subchain, \\exists l' \\in t.subchain, \\mathrm{length}(l) + n \\le \\mathrm{length}(l') + m $$$
Lean4
theorem chainHeight_add_le_chainHeight_add (s : Set α) (t : Set β) (n m : ℕ) :
s.chainHeight + n ≤ t.chainHeight + m ↔ ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, length l + n ≤ length l' + m :=
by
refine
⟨fun e l h ↦ le_chainHeight_add_nat_iff.1 ((add_le_add_right (length_le_chainHeight_of_mem_subchain h) _).trans e),
fun H ↦ ?_⟩
by_cases h : s.chainHeight = ⊤
· suffices t.chainHeight = ⊤ by
rw [this, top_add]
exact le_top
rw [chainHeight_eq_top_iff] at h ⊢
intro k
have := (le_chainHeight_TFAE t k).out 1 2
rw [this]
obtain ⟨l, hs, hl⟩ := h (k + m)
obtain ⟨l', ht, hl'⟩ := H l hs
exact ⟨l', ht, (add_le_add_iff_right m).1 <| _root_.trans (hl.symm.trans_le le_self_add) hl'⟩
· obtain ⟨k, hk⟩ := WithTop.ne_top_iff_exists.1 h
obtain ⟨l, hs, hl⟩ := le_chainHeight_iff.1 hk.le
rw [← hk, ← hl]
exact le_chainHeight_add_nat_iff.2 (H l hs)
