English
Let f be a partial function from α to β ⊕ α. If from input a one step forward yields a value in the left component, i.e. Sum.inl(b) ∈ f(a), then b appears in the fixed-point value f.fix(a).
Русский
Пусть f частичная функция от α в β ⊕ α. Если из аргумента a можно перейти на шаг вперед к элементу левой компоненты, то есть Sum.inl(b) ∈ f(a), то b принадлежит фиксированному значению f.fix(a).
LaTeX
$$$\\forall a:\\alpha,\\forall b:\\beta,\\; \\mathrm{inl}(b) \\in f(a) \\Rightarrow b \\in f.fix(a)$$$
Lean4
/-- If advancing one step from `a` leads to `b : β`, then `f.fix a = b` -/
theorem fix_stop {f : α →. β ⊕ α} {b : β} {a : α} (hb : Sum.inl b ∈ f a) : b ∈ f.fix a :=
by
rw [PFun.mem_fix_iff]
exact Or.inl hb
