English
Let α be a preorder with a top element and WellFoundedGT α. If P is a property on α such that there exists M with P(M) and whenever N ≠ ⊤ and P(N) holds there exists M > N with P(M), then P(⊤).
Русский
Пусть α упорядочено с верхней границей и имеется WellFoundedGT α. Пусть свойство P на α удовлетворяет: существует M с P(M), и для каждого N ≠ ⊤, P(N) влечёт существование M > N с P(M). Тогда выполняется P(⊤).
LaTeX
$$$(\\exists M\\ P(M)) \\to (\\forall N \\neq \\top\\, (P(N) \\to \\exists M > N\\, P(M))) \\to P(\\top)$$$
Lean4
@[elab_as_elim]
theorem induction_bot [Preorder α] [WellFoundedLT α] [OrderBot α] {P : α → Prop} (hexists : ∃ M, P M)
(hind : ∀ N ≠ ⊥, P N → ∃ M < N, P M) : P ⊥ := by
contrapose! hexists
intro M
induction M using WellFoundedLT.induction with
| ind x IH =>
by_cases hx : x = ⊥
· exact hx ▸ hexists
· intro hx'
obtain ⟨M, hM, hM'⟩ := hind x hx hx'
exact IH _ hM hM'
