ind_mk — Mathlib

English

Let C be a property of real numbers. If C holds for mk y for every CauSeq y, then C(x) holds for every Real x (quotient-induction principle).

Русский

Пусть C — свойство вещественных чисел. Если C выполняется для всех mk y, то для любого x, C(x) выполняется (принцип индукции на mk).

LaTeX

$$$\forall C:(\mathbb{R} \to \mathrm{Prop})\ (\forall y:\mathbb{R}, C(\mathrm{mk}(y))) \Rightarrow C(x)$$$

Lean4

@[elab_as_elim]
protected theorem ind_mk {C : Real → Prop} (x : Real) (h : ∀ y, C (mk y)) : C x :=
  by
  obtain ⟨x⟩ := x
  induction x using Quot.induction_on
  exact h _

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