English
Composition of two fundamental sequences is fundamental with a composed index function.
Русский
Суперпозиция двух фундаментальных последовательностей сохраняет фундаментальность.
LaTeX
$$$$\text{If } hf:\IsFundamentalSequence(a,o,f) \text{ and } hg:\IsFundamentalSequence(o,o',g) \text{ then } \IsFundamentalSequence(a,o',f\circ g).$$$$
Lean4
theorem trans {a o o' : Ordinal.{u}} {f : ∀ b < o, Ordinal.{u}} (hf : IsFundamentalSequence a o f)
{g : ∀ b < o', Ordinal.{u}} (hg : IsFundamentalSequence o o' g) :
IsFundamentalSequence a o' fun i hi => f (g i hi) (by rw [← hg.2.2]; apply lt_blsub) :=
by
refine ⟨?_, @fun i j _ _ h => hf.2.1 _ _ (hg.2.1 _ _ h), ?_⟩
· rw [hf.cof_eq]
exact hg.1.trans (ord_cof_le o)
· rw [@blsub_comp.{u, u, u} o _ f (@IsFundamentalSequence.monotone _ _ f hf)]
· exact hf.2.2
· exact hg.2.2
