English
Let α be a complete lattice and f: α → α monotone. For any predicate P on α, if P is preserved by f along steps below the lfp and is closed under suprema, then P holds at the least fixed point of f.
Русский
Пусть α — полная решётка, f: α → α монотонна. Для любых свойств P на α, если P сохраняется при переходе от a к f(a) для a ниже lfp и замыкается на супремумах, тогда P верно для наименьшей фиксированной точки.
LaTeX
$$$\text{Let } \alpha \text{ be a complete lattice and } f: \alpha \to \alpha.\ f \text{ is monotone. If } P: \alpha \to \text{Prop} \text{ satisfies: } \\ (1) \forall a, P(a) \Rightarrow P(f(a)) \text{ for } a \le \mathrm{lfp}(f), \\ (2) \forall S, (\forall a \in S, P(a)) \Rightarrow P(\sup S), \\text{then } P(\mathrm{lfp}(f)).$$$
Lean4
theorem lfp_induction {p : α → Prop} (step : ∀ a, p a → a ≤ f.lfp → p (f a)) (hSup : ∀ s, (∀ a ∈ s, p a) → p (sSup s)) :
p f.lfp := by
set s := {a | a ≤ f.lfp ∧ p a}
specialize hSup s fun a => And.right
suffices sSup s = f.lfp from this ▸ hSup
have h : sSup s ≤ f.lfp := sSup_le fun b => And.left
have hmem : f (sSup s) ∈ s := ⟨f.map_le_lfp h, step _ hSup h⟩
exact h.antisymm (f.lfp_le <| le_sSup hmem)
