English
Equivalence is preserved under the smash operation combining two CompositionSeries, given the requisite head/tail alignments and equivalences.
Русский
Эквивалентность сохраняется под операцией smash, объединяющей две композиционные последовательности, при наличии требуемого согласования голов и хвостов и эквивалентностей.
LaTeX
$$$\\forall s_1\\ s_2\\ t_1\\ t_2,\\; hs: s_1.last = s_2.head \\land ht: t_1.last = t_2.head \\land h\\_1: s_1.Equivalent t_1 \\land h\\_2: s_2.Equivalent t_2 \\Rightarrow\\ (smash s_1 s_2 hs) (smash t_1 t_2 ht).$$$
Lean4
/-- **Kőnig's infinity lemma** : if each element in a strongly atomic order
is covered by only finitely many others, and `b` is an element with infinitely many things above it,
then there is a sequence starting with `b` in which each element is covered by the next. -/
theorem exists_seq_covby_of_forall_covby_finite (hfin : ∀ (a : α), {x | a ⋖ x}.Finite) (hb : (Ici b).Infinite) :
∃ f : ℕ → α, f 0 = b ∧ ∀ i, f i ⋖ f (i + 1) :=
let h := fun a : { a : α // (Ici a).Infinite } ↦ exists_covby_infinite_Ici_of_infinite_Ici a.2 (hfin a)
let ks : ℕ → { a : α // (Ici a).Infinite } := Nat.rec ⟨b, hb⟩ fun _ a ↦ ⟨_, (h a).choose_spec.2⟩
⟨fun i ↦ (ks i).1, by simp [ks], fun i ↦ by simpa using (h (ks i)).choose_spec.1⟩
