Documentation

Mathlib.Data.Quot

Quotient types #

This module extends the core library's treatment of quotient types (Init.Core).

Tags #

quotient

instance Setoid.instCoeFunForallForallProp_mathlib {α : Sort u_1} :
CoeFun (Setoid α) fun (x : Setoid α) => ααProp

When writing a lemma about someSetoid x y (which uses this instance), call it someSetoid_apply not someSetoid_r.

Equations
    theorem Setoid.ext {α : Sort u_3} {s t : Setoid α} :
    (∀ (a b : α), s a b t a b)s = t
    theorem Quot.induction_on {α : Sort u_4} {r : ααProp} {β : Quot rProp} (q : Quot r) (h : ∀ (a : α), β (mk r a)) :
    β q
    instance Quot.instInhabited_mathlib {α : Sort u_1} (r : ααProp) [Inhabited α] :
    Equations
      instance Quot.Subsingleton {α : Sort u_1} {ra : ααProp} [Subsingleton α] :
      instance Quot.instUnique {α : Sort u_1} {ra : ααProp} [Unique α] :
      Equations
        def Quot.hrecOn₂ {α : Sort u_1} {β : Sort u_2} {ra : ααProp} {rb : ββProp} {φ : Quot raQuot rbSort u_3} (qa : Quot ra) (qb : Quot rb) (f : (a : α) → (b : β) → φ (mk ra a) (mk rb b)) (ca : ∀ {b : β} {a₁ a₂ : α}, ra a₁ a₂f a₁ b f a₂ b) (cb : ∀ {a : α} {b₁ b₂ : β}, rb b₁ b₂f a b₁ f a b₂) :
        φ qa qb

        Recursion on two Quotient arguments a and b, result type depends on ⟦a⟧ and ⟦b⟧.

        Equations
          Instances For
            def Quot.map {α : Sort u_1} {β : Sort u_2} {ra : ααProp} {rb : ββProp} (f : αβ) (h : ∀ ⦃a b : α⦄, ra a brb (f a) (f b)) :
            Quot raQuot rb

            Map a function f : α → β such that ra x y implies rb (f x) (f y) to a map Quot ra → Quot rb.

            Equations
              Instances For
                def Quot.mapRight {α : Sort u_1} {ra ra' : ααProp} (h : ∀ (a₁ a₂ : α), ra a₁ a₂ra' a₁ a₂) :
                Quot raQuot ra'

                If ra is a subrelation of ra', then we have a natural map Quot ra → Quot ra'.

                Equations
                  Instances For
                    def Quot.factor {α : Type u_4} (r s : ααProp) (h : ∀ (x y : α), r x ys x y) :
                    Quot rQuot s

                    Weaken the relation of a quotient. This is the same as Quot.map id.

                    Equations
                      Instances For
                        theorem Quot.factor_mk_eq {α : Type u_4} (r s : ααProp) (h : ∀ (x y : α), r x ys x y) :
                        factor r s h mk r = mk s
                        theorem Quot.lift_mk {α : Sort u_1} {γ : Sort u_4} {r : ααProp} (f : αγ) (h : ∀ (a₁ a₂ : α), r a₁ a₂f a₁ = f a₂) (a : α) :
                        lift f h (mk r a) = f a
                        theorem Quot.liftOn_mk {α : Sort u_1} {γ : Sort u_4} {r : ααProp} (a : α) (f : αγ) (h : ∀ (a₁ a₂ : α), r a₁ a₂f a₁ = f a₂) :
                        (mk r a).liftOn f h = f a
                        @[simp]
                        theorem Quot.surjective_lift {α : Sort u_1} {γ : Sort u_4} {r : ααProp} {f : αγ} (h : ∀ (a₁ a₂ : α), r a₁ a₂f a₁ = f a₂) :
                        def Quot.lift₂ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_4} {r : ααProp} {s : ββProp} (f : αβγ) (hr : ∀ (a : α) (b₁ b₂ : β), s b₁ b₂f a b₁ = f a b₂) (hs : ∀ (a₁ a₂ : α) (b : β), r a₁ a₂f a₁ b = f a₂ b) (q₁ : Quot r) (q₂ : Quot s) :
                        γ

                        Descends a function f : α → β → γ to quotients of α and β.

                        Equations
                          Instances For
                            @[simp]
                            theorem Quot.lift₂_mk {α : Sort u_1} {β : Sort u_2} {γ : Sort u_4} {r : ααProp} {s : ββProp} (f : αβγ) (hr : ∀ (a : α) (b₁ b₂ : β), s b₁ b₂f a b₁ = f a b₂) (hs : ∀ (a₁ a₂ : α) (b : β), r a₁ a₂f a₁ b = f a₂ b) (a : α) (b : β) :
                            Quot.lift₂ f hr hs (mk r a) (mk s b) = f a b
                            def Quot.liftOn₂ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_4} {r : ααProp} {s : ββProp} (p : Quot r) (q : Quot s) (f : αβγ) (hr : ∀ (a : α) (b₁ b₂ : β), s b₁ b₂f a b₁ = f a b₂) (hs : ∀ (a₁ a₂ : α) (b : β), r a₁ a₂f a₁ b = f a₂ b) :
                            γ

                            Descends a function f : α → β → γ to quotients of α and β and applies it.

                            Equations
                              Instances For
                                @[simp]
                                theorem Quot.liftOn₂_mk {α : Sort u_1} {β : Sort u_2} {γ : Sort u_4} {r : ααProp} {s : ββProp} (a : α) (b : β) (f : αβγ) (hr : ∀ (a : α) (b₁ b₂ : β), s b₁ b₂f a b₁ = f a b₂) (hs : ∀ (a₁ a₂ : α) (b : β), r a₁ a₂f a₁ b = f a₂ b) :
                                (mk r a).liftOn₂ (mk s b) f hr hs = f a b
                                def Quot.map₂ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_4} {r : ααProp} {s : ββProp} {t : γγProp} (f : αβγ) (hr : ∀ (a : α) (b₁ b₂ : β), s b₁ b₂t (f a b₁) (f a b₂)) (hs : ∀ (a₁ a₂ : α) (b : β), r a₁ a₂t (f a₁ b) (f a₂ b)) (q₁ : Quot r) (q₂ : Quot s) :

                                Descends a function f : α → β → γ to quotients of α and β with values in a quotient of γ.

                                Equations
                                  Instances For
                                    @[simp]
                                    theorem Quot.map₂_mk {α : Sort u_1} {β : Sort u_2} {γ : Sort u_4} {r : ααProp} {s : ββProp} {t : γγProp} (f : αβγ) (hr : ∀ (a : α) (b₁ b₂ : β), s b₁ b₂t (f a b₁) (f a b₂)) (hs : ∀ (a₁ a₂ : α) (b : β), r a₁ a₂t (f a₁ b) (f a₂ b)) (a : α) (b : β) :
                                    Quot.map₂ f hr hs (mk r a) (mk s b) = mk t (f a b)
                                    def Quot.recOnSubsingleton₂ {α : Sort u_1} {β : Sort u_2} {r : ααProp} {s : ββProp} {φ : Quot rQuot sSort u_5} [h : ∀ (a : α) (b : β), Subsingleton (φ (mk r a) (mk s b))] (q₁ : Quot r) (q₂ : Quot s) (f : (a : α) → (b : β) → φ (mk r a) (mk s b)) :
                                    φ q₁ q₂

                                    A binary version of Quot.recOnSubsingleton.

                                    Equations
                                      Instances For
                                        theorem Quot.induction_on₂ {α : Sort u_1} {β : Sort u_2} {r : ααProp} {s : ββProp} {δ : Quot rQuot sProp} (q₁ : Quot r) (q₂ : Quot s) (h : ∀ (a : α) (b : β), δ (mk r a) (mk s b)) :
                                        δ q₁ q₂
                                        theorem Quot.induction_on₃ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_4} {r : ααProp} {s : ββProp} {t : γγProp} {δ : Quot rQuot sQuot tProp} (q₁ : Quot r) (q₂ : Quot s) (q₃ : Quot t) (h : ∀ (a : α) (b : β) (c : γ), δ (mk r a) (mk s b) (mk t c)) :
                                        δ q₁ q₂ q₃
                                        instance Quot.lift.decidablePred {α : Sort u_1} (r : ααProp) (f : αProp) (h : ∀ (a b : α), r a bf a = f b) [hf : DecidablePred f] :
                                        Equations
                                          instance Quot.lift₂.decidablePred {α : Sort u_1} {β : Sort u_2} (r : ααProp) (s : ββProp) (f : αβProp) (ha : ∀ (a : α) (b₁ b₂ : β), s b₁ b₂f a b₁ = f a b₂) (hb : ∀ (a₁ a₂ : α) (b : β), r a₁ a₂f a₁ b = f a₂ b) [hf : (a : α) → DecidablePred (f a)] (q₁ : Quot r) :

                                          Note that this provides DecidableRel (Quot.Lift₂ f ha hb) when α = β.

                                          Equations
                                            instance Quot.instDecidableLiftOnOfDecidablePred_mathlib {α : Sort u_1} (r : ααProp) (q : Quot r) (f : αProp) (h : ∀ (a b : α), r a bf a = f b) [DecidablePred f] :
                                            Equations
                                              instance Quot.instDecidableLiftOn₂OfDecidablePred {α : Sort u_1} {β : Sort u_2} (r : ααProp) (s : ββProp) (q₁ : Quot r) (q₂ : Quot s) (f : αβProp) (ha : ∀ (a : α) (b₁ b₂ : β), s b₁ b₂f a b₁ = f a b₂) (hb : ∀ (a₁ a₂ : α) (b : β), r a₁ a₂f a₁ b = f a₂ b) [(a : α) → DecidablePred (f a)] :
                                              Decidable (q₁.liftOn₂ q₂ f ha hb)
                                              Equations

                                                Places an element of a type into the quotient that equates terms according to an equivalence relation.

                                                The setoid instance is provided explicitly. Quotient.mk' uses instance synthesis instead.

                                                Given v : α, Quotient.mk s v : Quotient s is like v, except all observations of v's value must respect s.r. Quotient.lift allows values in a quotient to be mapped to other types, so long as the mapping respects s.r.

                                                Equations
                                                  Instances For

                                                    Pretty printer defined by notation3 command.

                                                    Equations
                                                      Instances For
                                                        instance Quotient.instInhabitedQuotient {α : Sort u_1} (s : Setoid α) [Inhabited α] :
                                                        Equations
                                                          instance Quotient.instUniqueQuotient {α : Sort u_1} (s : Setoid α) [Unique α] :
                                                          Equations
                                                            instance Quotient.instIsEquivEquiv {α : Type u_4} [Setoid α] :
                                                            IsEquiv α fun (x1 x2 : α) => x1 x2
                                                            def Quotient.hrecOn₂ {α : Sort u_1} {β : Sort u_2} {sa : Setoid α} {sb : Setoid β} {φ : Quotient saQuotient sbSort u_3} (qa : Quotient sa) (qb : Quotient sb) (f : (a : α) → (b : β) → φ a b) (c : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ a₂b₁ b₂f a₁ b₁ f a₂ b₂) :
                                                            φ qa qb

                                                            Induction on two Quotient arguments a and b, result type depends on ⟦a⟧ and ⟦b⟧.

                                                            Equations
                                                              Instances For
                                                                def Quotient.map {α : Sort u_1} {β : Sort u_2} {sa : Setoid α} {sb : Setoid β} (f : αβ) (h : ∀ ⦃a b : α⦄, a bf a f b) :
                                                                Quotient saQuotient sb

                                                                Map a function f : α → β that sends equivalent elements to equivalent elements to a function Quotient sa → Quotient sb. Useful to define unary operations on quotients.

                                                                Equations
                                                                  Instances For
                                                                    @[simp]
                                                                    theorem Quotient.map_mk {α : Sort u_1} {β : Sort u_2} {sa : Setoid α} {sb : Setoid β} (f : αβ) (h : ∀ ⦃a b : α⦄, a bf a f b) (x : α) :
                                                                    def Quotient.map₂ {α : Sort u_1} {β : Sort u_2} {sa : Setoid α} {sb : Setoid β} {γ : Sort u_4} {sc : Setoid γ} (f : αβγ) (h : ∀ ⦃a₁ a₂ : α⦄, a₁ a₂∀ ⦃b₁ b₂ : β⦄, b₁ b₂f a₁ b₁ f a₂ b₂) :
                                                                    Quotient saQuotient sbQuotient sc

                                                                    Map a function f : α → β → γ that sends equivalent elements to equivalent elements to a function f : Quotient sa → Quotient sb → Quotient sc. Useful to define binary operations on quotients.

                                                                    Equations
                                                                      Instances For
                                                                        @[simp]
                                                                        theorem Quotient.map₂_mk {α : Sort u_1} {β : Sort u_2} {sa : Setoid α} {sb : Setoid β} {γ : Sort u_4} {sc : Setoid γ} (f : αβγ) (h : ∀ ⦃a₁ a₂ : α⦄, a₁ a₂∀ ⦃b₁ b₂ : β⦄, b₁ b₂f a₁ b₁ f a₂ b₂) (x : α) (y : β) :
                                                                        instance Quotient.lift.decidablePred {α : Sort u_1} {sa : Setoid α} (f : αProp) (h : ∀ (a b : α), a bf a = f b) [DecidablePred f] :
                                                                        Equations
                                                                          instance Quotient.lift₂.decidablePred {α : Sort u_1} {β : Sort u_2} {sa : Setoid α} {sb : Setoid β} (f : αβProp) (h : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ a₂b₁ b₂f a₁ b₁ = f a₂ b₂) [hf : (a : α) → DecidablePred (f a)] (q₁ : Quotient sa) :

                                                                          Note that this provides DecidableRel (Quotient.lift₂ f h) when α = β.

                                                                          Equations
                                                                            instance Quotient.instDecidableLiftOnOfDecidablePred_mathlib {α : Sort u_1} {sa : Setoid α} (q : Quotient sa) (f : αProp) (h : ∀ (a b : α), a bf a = f b) [DecidablePred f] :
                                                                            Equations
                                                                              instance Quotient.instDecidableLiftOn₂OfDecidablePred_mathlib {α : Sort u_1} {β : Sort u_2} {sa : Setoid α} {sb : Setoid β} (q₁ : Quotient sa) (q₂ : Quotient sb) (f : αβProp) (h : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ a₂b₁ b₂f a₁ b₁ = f a₂ b₂) [(a : α) → DecidablePred (f a)] :
                                                                              Decidable (q₁.liftOn₂ q₂ f h)
                                                                              Equations
                                                                                theorem Quot.eq {α : Type u_3} {r : ααProp} {x y : α} :
                                                                                mk r x = mk r y Relation.EqvGen r x y
                                                                                @[simp]
                                                                                theorem Quotient.eq {α : Sort u_1} {r : Setoid α} {x y : α} :
                                                                                x = y r x y
                                                                                theorem Quotient.eq_iff_equiv {α : Sort u_1} {r : Setoid α} {x y : α} :
                                                                                theorem Quotient.forall {α : Sort u_3} {s : Setoid α} {p : Quotient sProp} :
                                                                                (∀ (a : Quotient s), p a) ∀ (a : α), p a
                                                                                theorem Quotient.exists {α : Sort u_3} {s : Setoid α} {p : Quotient sProp} :
                                                                                ( (a : Quotient s), p a) (a : α), p a
                                                                                @[simp]
                                                                                theorem Quotient.lift_mk {α : Sort u_1} {β : Sort u_2} {s : Setoid α} (f : αβ) (h : ∀ (a b : α), a bf a = f b) (x : α) :
                                                                                @[simp]
                                                                                theorem Quotient.lift_comp_mk {α : Sort u_1} {β : Sort u_2} {x✝ : Setoid α} (f : αβ) (h : ∀ (a b : α), a bf a = f b) :
                                                                                @[simp]
                                                                                theorem Quotient.lift_surjective_iff {α : Sort u_3} {β : Sort u_4} {s : Setoid α} (f : αβ) (h : ∀ (a b : α), a bf a = f b) :
                                                                                theorem Quotient.lift_surjective {α : Sort u_3} {β : Sort u_4} {s : Setoid α} (f : αβ) (h : ∀ (a b : α), a bf a = f b) (hf : Function.Surjective f) :
                                                                                @[simp]
                                                                                theorem Quotient.lift₂_mk {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} {x✝ : Setoid α} {x✝¹ : Setoid β} (f : αβγ) (h : ∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), a₁ b₁a₂ b₂f a₁ a₂ = f b₁ b₂) (a : α) (b : β) :
                                                                                theorem Quotient.liftOn_mk {α : Sort u_1} {β : Sort u_2} {s : Setoid α} (f : αβ) (h : ∀ (a b : α), a bf a = f b) (x : α) :
                                                                                x.liftOn f h = f x
                                                                                @[simp]
                                                                                theorem Quotient.liftOn₂_mk {α : Sort u_3} {β : Sort u_4} {x✝ : Setoid α} (f : ααβ) (h : ∀ (a₁ a₂ b₁ b₂ : α), a₁ b₁a₂ b₂f a₁ a₂ = f b₁ b₂) (x y : α) :
                                                                                x.liftOn₂ y f h = f x y
                                                                                theorem Quot.mk_surjective {α : Sort u_1} {r : ααProp} :

                                                                                Quot.mk r is a surjective function.

                                                                                Quotient.mk is a surjective function.

                                                                                Quotient.mk' is a surjective function.

                                                                                noncomputable def Quot.out {α : Sort u_1} {r : ααProp} (q : Quot r) :
                                                                                α

                                                                                Choose an element of the equivalence class using the axiom of choice. Sound but noncomputable.

                                                                                Equations
                                                                                  Instances For
                                                                                    unsafe def Quot.unquot {α : Sort u_1} {r : ααProp} :
                                                                                    Quot rα

                                                                                    Unwrap the VM representation of a quotient to obtain an element of the equivalence class. Computable but unsound.

                                                                                    Equations
                                                                                      Instances For
                                                                                        @[simp]
                                                                                        theorem Quot.out_eq {α : Sort u_1} {r : ααProp} (q : Quot r) :
                                                                                        mk r q.out = q
                                                                                        noncomputable def Quotient.out {α : Sort u_1} {s : Setoid α} :
                                                                                        Quotient sα

                                                                                        Choose an element of the equivalence class using the axiom of choice. Sound but noncomputable.

                                                                                        Equations
                                                                                          Instances For
                                                                                            @[simp]
                                                                                            theorem Quotient.out_eq {α : Sort u_1} {s : Setoid α} (q : Quotient s) :
                                                                                            theorem Quotient.mk_out {α : Sort u_1} {s : Setoid α} (a : α) :
                                                                                            s a.out a
                                                                                            theorem Quotient.mk_eq_iff_out {α : Sort u_1} {s : Setoid α} {x : α} {y : Quotient s} :
                                                                                            x = y x y.out
                                                                                            theorem Quotient.eq_mk_iff_out {α : Sort u_1} {s : Setoid α} {x : Quotient s} {y : α} :
                                                                                            x = y x.out y
                                                                                            @[simp]
                                                                                            theorem Quotient.out_equiv_out {α : Sort u_1} {s : Setoid α} {x y : Quotient s} :
                                                                                            x.out y.out x = y
                                                                                            @[simp]
                                                                                            theorem Quotient.out_inj {α : Sort u_1} {s : Setoid α} {x y : Quotient s} :
                                                                                            x.out = y.out x = y
                                                                                            instance piSetoid {ι : Sort u_3} {α : ιSort u_4} [(i : ι) → Setoid (α i)] :
                                                                                            Setoid ((i : ι) → α i)
                                                                                            Equations
                                                                                              def Quotient.eval {ι : Type u_3} {α : ιSort u_4} {S : (i : ι) → Setoid (α i)} (q : Quotient inferInstance) (i : ι) :
                                                                                              Quotient (S i)

                                                                                              Given a class of functions q : @Quotient (∀ i, α i) _, returns the class of i-th projection Quotient (S i).

                                                                                              Equations
                                                                                                Instances For
                                                                                                  @[simp]
                                                                                                  theorem Quotient.eval_mk {ι : Type u_3} {α : ιType u_4} {S : (i : ι) → Setoid (α i)} (f : (i : ι) → α i) :
                                                                                                  f.eval = fun (i : ι) => f i
                                                                                                  noncomputable def Quotient.choice {ι : Type u_3} {α : ιType u_4} {S : (i : ι) → Setoid (α i)} (f : (i : ι) → Quotient (S i)) :

                                                                                                  Given a function f : Π i, Quotient (S i), returns the class of functions Π i, α i sending each i to an element of the class f i.

                                                                                                  Equations
                                                                                                    Instances For
                                                                                                      @[simp]
                                                                                                      theorem Quotient.choice_eq {ι : Type u_3} {α : ιType u_4} {S : (i : ι) → Setoid (α i)} (f : (i : ι) → α i) :
                                                                                                      (choice fun (i : ι) => f i) = f
                                                                                                      theorem Quotient.induction_on_pi {ι : Type u_3} {α : ιSort u_4} {s : (i : ι) → Setoid (α i)} {p : ((i : ι) → Quotient (s i))Prop} (f : (i : ι) → Quotient (s i)) (h : ∀ (a : (i : ι) → α i), p fun (i : ι) => a i) :
                                                                                                      p f

                                                                                                      Truncation #

                                                                                                      theorem true_equivalence {α : Sort u_1} :
                                                                                                      Equivalence fun (x x : α) => True
                                                                                                      def trueSetoid {α : Sort u_1} :

                                                                                                      Always-true relation as a Setoid.

                                                                                                      Note that in later files the preferred spelling is ⊤ : Setoid α.

                                                                                                      Equations
                                                                                                        Instances For
                                                                                                          def Trunc (α : Sort u) :

                                                                                                          Trunc α is the quotient of α by the always-true relation. This is related to the propositional truncation in HoTT, and is similar in effect to Nonempty α, but unlike Nonempty α, Trunc α is data, so the VM representation is the same as α, and so this can be used to maintain computability.

                                                                                                          Equations
                                                                                                            Instances For
                                                                                                              def Trunc.mk {α : Sort u_1} (a : α) :

                                                                                                              Constructor for Trunc α

                                                                                                              Equations
                                                                                                                Instances For
                                                                                                                  instance Trunc.instInhabited {α : Sort u_1} [Inhabited α] :
                                                                                                                  Equations
                                                                                                                    def Trunc.lift {α : Sort u_1} {β : Sort u_2} (f : αβ) (c : ∀ (a b : α), f a = f b) :
                                                                                                                    Trunc αβ

                                                                                                                    Any constant function lifts to a function out of the truncation

                                                                                                                    Equations
                                                                                                                      Instances For
                                                                                                                        theorem Trunc.ind {α : Sort u_1} {β : Trunc αProp} :
                                                                                                                        (∀ (a : α), β (mk a))∀ (q : Trunc α), β q
                                                                                                                        theorem Trunc.lift_mk {α : Sort u_1} {β : Sort u_2} (f : αβ) (c : ∀ (a b : α), f a = f b) (a : α) :
                                                                                                                        lift f c (mk a) = f a
                                                                                                                        def Trunc.liftOn {α : Sort u_1} {β : Sort u_2} (q : Trunc α) (f : αβ) (c : ∀ (a b : α), f a = f b) :
                                                                                                                        β

                                                                                                                        Lift a constant function on q : Trunc α.

                                                                                                                        Equations
                                                                                                                          Instances For
                                                                                                                            theorem Trunc.induction_on {α : Sort u_1} {β : Trunc αProp} (q : Trunc α) (h : ∀ (a : α), β (mk a)) :
                                                                                                                            β q
                                                                                                                            theorem Trunc.exists_rep {α : Sort u_1} (q : Trunc α) :
                                                                                                                            (a : α), mk a = q
                                                                                                                            theorem Trunc.induction_on₂ {α : Sort u_1} {β : Sort u_2} {C : Trunc αTrunc βProp} (q₁ : Trunc α) (q₂ : Trunc β) (h : ∀ (a : α) (b : β), C (mk a) (mk b)) :
                                                                                                                            C q₁ q₂
                                                                                                                            theorem Trunc.eq {α : Sort u_1} (a b : Trunc α) :
                                                                                                                            a = b
                                                                                                                            def Trunc.bind {α : Sort u_1} {β : Sort u_2} (q : Trunc α) (f : αTrunc β) :

                                                                                                                            The bind operator for the Trunc monad.

                                                                                                                            Equations
                                                                                                                              Instances For
                                                                                                                                def Trunc.map {α : Sort u_1} {β : Sort u_2} (f : αβ) (q : Trunc α) :

                                                                                                                                A function f : α → β defines a function map f : Trunc α → Trunc β.

                                                                                                                                Equations
                                                                                                                                  Instances For
                                                                                                                                    Equations
                                                                                                                                      def Trunc.rec {α : Sort u_1} {C : Trunc αSort u_3} (f : (a : α) → C (mk a)) (h : ∀ (a b : α), f a = f b) (q : Trunc α) :
                                                                                                                                      C q

                                                                                                                                      Recursion/induction principle for Trunc.

                                                                                                                                      Equations
                                                                                                                                        Instances For
                                                                                                                                          def Trunc.recOn {α : Sort u_1} {C : Trunc αSort u_3} (q : Trunc α) (f : (a : α) → C (mk a)) (h : ∀ (a b : α), f a = f b) :
                                                                                                                                          C q

                                                                                                                                          A version of Trunc.rec taking q : Trunc α as the first argument.

                                                                                                                                          Equations
                                                                                                                                            Instances For
                                                                                                                                              def Trunc.recOnSubsingleton {α : Sort u_1} {C : Trunc αSort u_3} [∀ (a : α), Subsingleton (C (mk a))] (q : Trunc α) (f : (a : α) → C (mk a)) :
                                                                                                                                              C q

                                                                                                                                              A version of Trunc.recOn assuming the codomain is a Subsingleton.

                                                                                                                                              Equations
                                                                                                                                                Instances For
                                                                                                                                                  noncomputable def Trunc.out {α : Sort u_1} :
                                                                                                                                                  Trunc αα

                                                                                                                                                  Noncomputably extract a representative of Trunc α (using the axiom of choice).

                                                                                                                                                  Equations
                                                                                                                                                    Instances For
                                                                                                                                                      @[simp]
                                                                                                                                                      theorem Trunc.out_eq {α : Sort u_1} (q : Trunc α) :
                                                                                                                                                      mk q.out = q
                                                                                                                                                      theorem Trunc.nonempty {α : Sort u_1} (q : Trunc α) :

                                                                                                                                                      Quotient with implicit Setoid #

                                                                                                                                                      Versions of quotient definitions and lemmas ending in ' use unification instead of typeclass inference for inferring the Setoid argument. This is useful when there are several different quotient relations on a type, for example quotient groups, rings and modules.

                                                                                                                                                      @[reducible, inline]
                                                                                                                                                      abbrev Quotient.mk'' {α : Sort u_1} {s₁ : Setoid α} (a : α) :

                                                                                                                                                      A version of Quotient.mk taking {s : Setoid α} as an implicit argument instead of an instance argument.

                                                                                                                                                      Equations
                                                                                                                                                        Instances For

                                                                                                                                                          Quotient.mk'' is a surjective function.

                                                                                                                                                          def Quotient.liftOn' {α : Sort u_1} {φ : Sort u_4} {s₁ : Setoid α} (q : Quotient s₁) (f : αφ) (h : ∀ (a b : α), s₁ a bf a = f b) :
                                                                                                                                                          φ

                                                                                                                                                          A version of Quotient.liftOn taking {s : Setoid α} as an implicit argument instead of an instance argument.

                                                                                                                                                          Equations
                                                                                                                                                            Instances For
                                                                                                                                                              @[simp]
                                                                                                                                                              theorem Quotient.liftOn'_mk'' {α : Sort u_1} {φ : Sort u_4} {s₁ : Setoid α} (f : αφ) (h : ∀ (a b : α), s₁ a bf a = f b) (x : α) :
                                                                                                                                                              (Quotient.mk'' x).liftOn' f h = f x
                                                                                                                                                              @[simp]
                                                                                                                                                              theorem Quotient.surjective_liftOn' {α : Sort u_1} {φ : Sort u_4} {s₁ : Setoid α} {f : αφ} (h : ∀ (a b : α), s₁ a bf a = f b) :
                                                                                                                                                              def Quotient.liftOn₂' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {s₁ : Setoid α} {s₂ : Setoid β} (q₁ : Quotient s₁) (q₂ : Quotient s₂) (f : αβγ) (h : ∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), s₁ a₁ b₁s₂ a₂ b₂f a₁ a₂ = f b₁ b₂) :
                                                                                                                                                              γ

                                                                                                                                                              A version of Quotient.liftOn₂ taking {s₁ : Setoid α} {s₂ : Setoid β} as implicit arguments instead of instance arguments.

                                                                                                                                                              Equations
                                                                                                                                                                Instances For
                                                                                                                                                                  @[simp]
                                                                                                                                                                  theorem Quotient.liftOn₂'_mk'' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {s₁ : Setoid α} {s₂ : Setoid β} (f : αβγ) (h : ∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), s₁ a₁ b₁s₂ a₂ b₂f a₁ a₂ = f b₁ b₂) (a : α) (b : β) :
                                                                                                                                                                  theorem Quotient.ind' {α : Sort u_1} {s₁ : Setoid α} {p : Quotient s₁Prop} (h : ∀ (a : α), p (Quotient.mk'' a)) (q : Quotient s₁) :
                                                                                                                                                                  p q

                                                                                                                                                                  A version of Quotient.ind taking {s : Setoid α} as an implicit argument instead of an instance argument.

                                                                                                                                                                  theorem Quotient.ind₂' {α : Sort u_1} {β : Sort u_2} {s₁ : Setoid α} {s₂ : Setoid β} {p : Quotient s₁Quotient s₂Prop} (h : ∀ (a₁ : α) (a₂ : β), p (Quotient.mk'' a₁) (Quotient.mk'' a₂)) (q₁ : Quotient s₁) (q₂ : Quotient s₂) :
                                                                                                                                                                  p q₁ q₂

                                                                                                                                                                  A version of Quotient.ind₂ taking {s₁ : Setoid α} {s₂ : Setoid β} as implicit arguments instead of instance arguments.

                                                                                                                                                                  theorem Quotient.inductionOn' {α : Sort u_1} {s₁ : Setoid α} {p : Quotient s₁Prop} (q : Quotient s₁) (h : ∀ (a : α), p (Quotient.mk'' a)) :
                                                                                                                                                                  p q

                                                                                                                                                                  A version of Quotient.inductionOn taking {s : Setoid α} as an implicit argument instead of an instance argument.

                                                                                                                                                                  theorem Quotient.inductionOn₂' {α : Sort u_1} {β : Sort u_2} {s₁ : Setoid α} {s₂ : Setoid β} {p : Quotient s₁Quotient s₂Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂) (h : ∀ (a₁ : α) (a₂ : β), p (Quotient.mk'' a₁) (Quotient.mk'' a₂)) :
                                                                                                                                                                  p q₁ q₂

                                                                                                                                                                  A version of Quotient.inductionOn₂ taking {s₁ : Setoid α} {s₂ : Setoid β} as implicit arguments instead of instance arguments.

                                                                                                                                                                  theorem Quotient.inductionOn₃' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {s₁ : Setoid α} {s₂ : Setoid β} {s₃ : Setoid γ} {p : Quotient s₁Quotient s₂Quotient s₃Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂) (q₃ : Quotient s₃) (h : ∀ (a₁ : α) (a₂ : β) (a₃ : γ), p (Quotient.mk'' a₁) (Quotient.mk'' a₂) (Quotient.mk'' a₃)) :
                                                                                                                                                                  p q₁ q₂ q₃

                                                                                                                                                                  A version of Quotient.inductionOn₃ taking {s₁ : Setoid α} {s₂ : Setoid β} {s₃ : Setoid γ} as implicit arguments instead of instance arguments.

                                                                                                                                                                  def Quotient.recOnSubsingleton' {α : Sort u_1} {s₁ : Setoid α} {φ : Quotient s₁Sort u_5} [∀ (a : α), Subsingleton (φ a)] (q : Quotient s₁) (f : (a : α) → φ (Quotient.mk'' a)) :
                                                                                                                                                                  φ q

                                                                                                                                                                  A version of Quotient.recOnSubsingleton taking {s₁ : Setoid α} as an implicit argument instead of an instance argument.

                                                                                                                                                                  Equations
                                                                                                                                                                    Instances For
                                                                                                                                                                      def Quotient.recOnSubsingleton₂' {α : Sort u_1} {β : Sort u_2} {s₁ : Setoid α} {s₂ : Setoid β} {φ : Quotient s₁Quotient s₂Sort u_5} [∀ (a : α) (b : β), Subsingleton (φ a b)] (q₁ : Quotient s₁) (q₂ : Quotient s₂) (f : (a₁ : α) → (a₂ : β) → φ (Quotient.mk'' a₁) (Quotient.mk'' a₂)) :
                                                                                                                                                                      φ q₁ q₂

                                                                                                                                                                      A version of Quotient.recOnSubsingleton₂ taking {s₁ : Setoid α} {s₂ : Setoid α} as implicit arguments instead of instance arguments.

                                                                                                                                                                      Equations
                                                                                                                                                                        Instances For
                                                                                                                                                                          def Quotient.hrecOn' {α : Sort u_1} {s₁ : Setoid α} {φ : Quotient s₁Sort u_5} (qa : Quotient s₁) (f : (a : α) → φ (Quotient.mk'' a)) (c : ∀ (a₁ a₂ : α), a₁ a₂f a₁ f a₂) :
                                                                                                                                                                          φ qa

                                                                                                                                                                          Recursion on a Quotient argument a, result type depends on ⟦a⟧.

                                                                                                                                                                          Equations
                                                                                                                                                                            Instances For
                                                                                                                                                                              @[simp]
                                                                                                                                                                              theorem Quotient.hrecOn'_mk'' {α : Sort u_1} {s₁ : Setoid α} {φ : Quotient s₁Sort u_5} (f : (a : α) → φ (Quotient.mk'' a)) (c : ∀ (a₁ a₂ : α), a₁ a₂f a₁ f a₂) (x : α) :
                                                                                                                                                                              (Quotient.mk'' x).hrecOn' f c = f x
                                                                                                                                                                              def Quotient.hrecOn₂' {α : Sort u_1} {β : Sort u_2} {s₁ : Setoid α} {s₂ : Setoid β} {φ : Quotient s₁Quotient s₂Sort u_5} (qa : Quotient s₁) (qb : Quotient s₂) (f : (a : α) → (b : β) → φ (Quotient.mk'' a) (Quotient.mk'' b)) (c : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ a₂b₁ b₂f a₁ b₁ f a₂ b₂) :
                                                                                                                                                                              φ qa qb

                                                                                                                                                                              Recursion on two Quotient arguments a and b, result type depends on ⟦a⟧ and ⟦b⟧.

                                                                                                                                                                              Equations
                                                                                                                                                                                Instances For
                                                                                                                                                                                  @[simp]
                                                                                                                                                                                  theorem Quotient.hrecOn₂'_mk'' {α : Sort u_1} {β : Sort u_2} {s₁ : Setoid α} {s₂ : Setoid β} {φ : Quotient s₁Quotient s₂Sort u_5} (f : (a : α) → (b : β) → φ (Quotient.mk'' a) (Quotient.mk'' b)) (c : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ a₂b₁ b₂f a₁ b₁ f a₂ b₂) (x : α) (qb : Quotient s₂) :
                                                                                                                                                                                  (Quotient.mk'' x).hrecOn₂' qb f c = qb.hrecOn' (f x)
                                                                                                                                                                                  def Quotient.map' {α : Sort u_1} {β : Sort u_2} {s₁ : Setoid α} {s₂ : Setoid β} (f : αβ) (h : ∀ (a b : α), s₁ a bs₂ (f a) (f b)) :
                                                                                                                                                                                  Quotient s₁Quotient s₂

                                                                                                                                                                                  Map a function f : α → β that sends equivalent elements to equivalent elements to a function Quotient sa → Quotient sb. Useful to define unary operations on quotients.

                                                                                                                                                                                  Equations
                                                                                                                                                                                    Instances For
                                                                                                                                                                                      @[simp]
                                                                                                                                                                                      theorem Quotient.map'_mk'' {α : Sort u_1} {β : Sort u_2} {s₁ : Setoid α} {s₂ : Setoid β} (f : αβ) (h : ∀ (a b : α), s₁ a bs₂ (f a) (f b)) (x : α) :
                                                                                                                                                                                      @[deprecated Quotient.map₂ (since := "2024-12-01")]
                                                                                                                                                                                      def Quotient.map₂' {α : Sort u_1} {β : Sort u_2} {sa : Setoid α} {sb : Setoid β} {γ : Sort u_4} {sc : Setoid γ} (f : αβγ) (h : ∀ ⦃a₁ a₂ : α⦄, a₁ a₂∀ ⦃b₁ b₂ : β⦄, b₁ b₂f a₁ b₁ f a₂ b₂) :
                                                                                                                                                                                      Quotient saQuotient sbQuotient sc

                                                                                                                                                                                      A version of Quotient.map₂ using curly braces and unification.

                                                                                                                                                                                      Equations
                                                                                                                                                                                        Instances For
                                                                                                                                                                                          theorem Quotient.exact' {α : Sort u_1} {s₁ : Setoid α} {a b : α} :
                                                                                                                                                                                          Quotient.mk'' a = Quotient.mk'' bs₁ a b
                                                                                                                                                                                          theorem Quotient.sound' {α : Sort u_1} {s₁ : Setoid α} {a b : α} :
                                                                                                                                                                                          s₁ a bQuotient.mk'' a = Quotient.mk'' b
                                                                                                                                                                                          @[simp]
                                                                                                                                                                                          theorem Quotient.eq' {α : Sort u_1} {s₁ : Setoid α} {a b : α} :
                                                                                                                                                                                          theorem Quotient.eq'' {α : Sort u_1} {s₁ : Setoid α} {a b : α} :
                                                                                                                                                                                          theorem Quotient.out_eq' {α : Sort u_1} {s₁ : Setoid α} (q : Quotient s₁) :
                                                                                                                                                                                          theorem Quotient.mk_out' {α : Sort u_1} {s₁ : Setoid α} (a : α) :
                                                                                                                                                                                          s₁ (Quotient.mk'' a).out a
                                                                                                                                                                                          @[simp]
                                                                                                                                                                                          theorem Quotient.liftOn'_mk {α : Sort u_1} {β : Sort u_2} {s : Setoid α} (x : α) (f : αβ) (h : ∀ (a b : α), s a bf a = f b) :
                                                                                                                                                                                          x.liftOn' f h = f x
                                                                                                                                                                                          @[simp]
                                                                                                                                                                                          theorem Quotient.liftOn₂'_mk {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {s : Setoid α} {t : Setoid β} (f : αβγ) (h : ∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), s a₁ b₁t a₂ b₂f a₁ a₂ = f b₁ b₂) (a : α) (b : β) :
                                                                                                                                                                                          theorem Quotient.map'_mk {α : Sort u_1} {β : Sort u_2} {s : Setoid α} {t : Setoid β} (f : αβ) (h : ∀ (a b : α), s a bt (f a) (f b)) (x : α) :
                                                                                                                                                                                          instance Quotient.instDecidableLiftOn'OfDecidablePred {α : Sort u_1} {s₁ : Setoid α} (q : Quotient s₁) (f : αProp) (h : ∀ (a b : α), s₁ a bf a = f b) [DecidablePred f] :
                                                                                                                                                                                          Equations
                                                                                                                                                                                            instance Quotient.instDecidableLiftOn₂'OfDecidablePred {α : Sort u_1} {β : Sort u_2} {s₁ : Setoid α} {s₂ : Setoid β} (q₁ : Quotient s₁) (q₂ : Quotient s₂) (f : αβProp) (h : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), s₁ a₁ a₂s₂ b₁ b₂f a₁ b₁ = f a₂ b₂) [(a : α) → DecidablePred (f a)] :
                                                                                                                                                                                            Decidable (q₁.liftOn₂' q₂ f h)
                                                                                                                                                                                            Equations
                                                                                                                                                                                              @[simp]
                                                                                                                                                                                              theorem Equivalence.quot_mk_eq_iff {α : Type u_3} {r : ααProp} (h : Equivalence r) (x y : α) :
                                                                                                                                                                                              Quot.mk r x = Quot.mk r y r x y