rec_bot — Mathlib

English

Given a predicate p on α with a bottom element, if p holds at bottom and is preserved by succ, then p holds for all a.

Русский

Для p на α, имеющего нижний элемент, если p(⊥) и p(a) ⇒ p(succ a) для всех a, то p(a) выполняется для любого a.

LaTeX

$$$ p(\bot) \land (\forall a, p(a) \to p(\operatorname{succ} a)) \Rightarrow \forall a, p(a).$$$

Lean4

theorem rec_bot (p : α → Prop) (hbot : p ⊥) (hsucc : ∀ a, p a → p (succ a)) (a : α) : p a :=
  Succ.rec hbot (fun x _ h => hsucc x h) (bot_le : ⊥ ≤ a)

Похожие утверждения