induction_on — Mathlib

English

For a property p on the completion space, if the set {a : hatα | p a} is closed and p holds on all ι a, then p holds for the given a.

Русский

Для свойства p на дополненном пространстве, если множество {a: hatα | p a} замкнуто и p выполняется на всех ι a, то p выполняется для данного a.

LaTeX

$$$IsClosed\\{a : \\hat{\\alpha} \\mid p(a)\\} \\to (\\forall a, p(\\iota(a))) \\to p(a)$$$

Lean4

@[elab_as_elim]
theorem induction_on {p : hatα → Prop} (a : hatα) (hp : IsClosed {a | p a}) (ih : ∀ a, p (ι a)) : p a :=
  isClosed_property pkg.dense hp ih a

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