induction_on — Mathlib

English

An induction principle allows proving a property for all angles by proving it for all real numbers under the natural embedding.

Русский

Принцип индукции по углам: если свойство верно для всех вещественных чисел через вложение в угол, то верно и для произвольного угла.

LaTeX

$$$$ \forall \theta\in\text{Angle},\ \big(\forall x\in\mathbb{R},\ P(\mathrm{Real.Angle.co e} x)\big) \to P(\theta). $$$$

Lean4

/-- An induction principle to deduce results for `Angle` from those for `ℝ`, used with
`induction θ using Real.Angle.induction_on`. -/
@[elab_as_elim]
protected theorem induction_on {p : Angle → Prop} (θ : Angle) (h : ∀ x : ℝ, p x) : p θ :=
  Quotient.inductionOn' θ h

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