induction_on — Mathlib

English

Induction principle on Completion α: if a predicate p on Completion α is closed, and holds on all coe a, then it holds for all elements of Completion α.

Русский

Принцип индукции по Completion α: если свойство p на Completion α замкнуто и выполняется для всех coe a, то выполняется для всех элементов Completion α.

LaTeX

$$$\\text{IsClosed}(\\{x:\\mathrm{Completion}(\\alpha) \\mid p(x)\\}) \\\\land\\ \\forall a:\\alpha,\\ p(\\mathrm{coe}'a) \\Rightarrow \\forall x:\\mathrm{Completion}(\\alpha),\\ p(x)$$$

Lean4

@[elab_as_elim]
theorem induction_on {p : Completion α → Prop} (a : Completion α) (hp : IsClosed {a | p a}) (ih : ∀ a : α, p a) : p a :=
  isClosed_property denseRange_coe hp ih a

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