From 445fd417be4df8f69f1b97b5426bd5ef97d28138 Mon Sep 17 00:00:00 2001 From: Bulhwi Cha Date: Mon, 20 Feb 2023 09:59:29 +0900 Subject: [PATCH] doc: add more explanations of quotients Add explanations of `Quotient.ind` and `Quotient.inductionOn` to `Init.Core`. --- src/Init/Core.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/Init/Core.lean b/src/Init/Core.lean index edb7be93a9..a4304ecb1c 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -1344,6 +1344,7 @@ then it lifts to a function on `Quotient s` such that `lift f h (mk a) = f a`. protected abbrev lift {α : Sort u} {β : Sort v} {s : Setoid α} (f : α → β) : ((a b : α) → a ≈ b → f a = f b) → Quotient s → β := Quot.lift f +/-- The analogue of `Quot.ind`: every element of `Quotient s` is of the form `Quotient.mk s a`. -/ protected theorem ind {α : Sort u} {s : Setoid α} {motive : Quotient s → Prop} : ((a : α) → motive (Quotient.mk s a)) → (q : Quotient s) → motive q := Quot.ind @@ -1354,6 +1355,7 @@ then it lifts to a function on `Quotient s` such that `lift (mk a) f h = f a`. protected abbrev liftOn {α : Sort u} {β : Sort v} {s : Setoid α} (q : Quotient s) (f : α → β) (c : (a b : α) → a ≈ b → f a = f b) : β := Quot.liftOn q f c +/-- The analogue of `Quot.inductionOn`: every element of `Quotient s` is of the form `Quotient.mk s a`. -/ @[elab_as_elim] protected theorem inductionOn {α : Sort u} {s : Setoid α} {motive : Quotient s → Prop} (q : Quotient s)