English
Blsub o' g composed with f equals Blsub o f under a suitable equality of bsup/bsub shifts.
Русский
Blsub o' g после композиции с f равен Blsub o f при подходящем равенстве смещений bsup/blsub.
LaTeX
$$$ (blsub( o',\\lambda a ha => f(g(a,ha)))) = blsub(o, f) $$$
Lean4
theorem blsub_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) :
(blsub.{_, w} o' fun a ha => f (g a ha) (by rw [← hg]; apply lt_blsub)) = blsub.{_, w} o f :=
@bsup_comp.{u, v, w} o _ (fun a ha => succ (f a ha)) (fun {_ _} _ _ h => succ_le_succ_iff.2 (hf _ _ h)) g hg
