English
If g is a function with o'.blsub g = o, then composing f with g inside bsup/o yields the same bsup as f on o.
Русский
Если g такова, что o'.blsub g = o, то композиция f с g внутри bsup/ o даёт тот же bsup, что и f на o.
LaTeX
$$$ (bsup( o',\\lambda a, ha => f(g(a,ha))(lt)) = bsup(o, f) $$$
Lean4
theorem bsup_comp {o o' : Ordinal.{max u v}} {f : ∀ a < o, Ordinal.{max u v w}}
(hf : ∀ {i j} (hi) (hj), i ≤ j → f i hi ≤ f j hj) {g : ∀ a < o', Ordinal.{max u v}} (hg : blsub.{_, u} o' g = o) :
(bsup.{_, w} o' fun a ha => f (g a ha) (by rw [← hg]; apply lt_blsub)) = bsup.{_, w} o f :=
by
apply le_antisymm <;> refine bsup_le fun i hi => ?_
· apply le_bsup
· rw [← hg, lt_blsub_iff] at hi
rcases hi with ⟨j, hj, hj'⟩
exact (hf _ _ hj').trans (le_bsup _ _ _)
