English
If b is in f.fix(a) and a' is the forward step from a (Sum.inr(a') ∈ f(a)), then b is in f.fix(a').
Русский
Если b принадлежит f.fix(a) и a' является прямым переходом из a (Sum.inr(a') ∈ f(a)), то b ∈ f.fix(a').
LaTeX
$$$\\forall f:\\,\\alpha \\to. (\\beta \\oplus \\alpha),\\; b:\\beta,\\; a,a' : \\alpha,\\; (b \\in f.fix(a)) \\rightarrow (\\mathrm{inr}(a') \\in f(a)) \\rightarrow b \\in f.fix(a')$$$
Lean4
theorem fix_fwd {f : α →. β ⊕ α} {b : β} {a a' : α} (hb : b ∈ f.fix a) (ha' : Sum.inr a' ∈ f a) : b ∈ f.fix a' := by
rwa [← fix_fwd_eq ha']