English
If advancing one step from a via f produces a' (i.e., Sum.inr(a') ∈ f(a)), then the fixed-point values at a and at a' are equal: f.fix(a) = f.fix(a').
Русский
Если при переходе на один шаг из a по f получается a' (Sum.inr(a') ∈ f(a)), то фиксированные значения в точках a и a' равны: f.fix(a) = f.fix(a').
LaTeX
$$$\\forall a,a' : \\alpha,\\; (\\mathrm{inr}(a') \\in f(a)) \\Rightarrow f.fix(a) = f.fix(a')$$$
Lean4
/-- If advancing one step from `a` on `f` leads to `a' : α`, then `f.fix a = f.fix a'` -/
theorem fix_fwd_eq {f : α →. β ⊕ α} {a a' : α} (ha' : Sum.inr a' ∈ f a) : f.fix a = f.fix a' :=
by
ext b; constructor
· intro h
obtain h' | ⟨a, h', e'⟩ := mem_fix_iff.1 h <;> cases Part.mem_unique ha' h'
exact e'
· intro h
rw [PFun.mem_fix_iff]
exact Or.inr ⟨a', ha', h⟩
