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 _