Documentation

Mathlib.Logic.Equiv.Defs

Equivalence between types #

In this file we define two types:

Then we define

Many more such isomorphisms and operations are defined in Logic.Equiv.Basic.

Tags #

equivalence, congruence, bijective map

structure Equiv (α : Sort u_1) (β : Sort u_2) :
Sort (max (max 1 u_1) u_2)

α ≃ β is the type of functions from α → β with a two-sided inverse.

Instances For
    theorem Equiv.left_inv {α : Sort u_1} {β : Sort u_2} (self : α β) :
    Function.LeftInverse self.invFun self.toFun
    theorem Equiv.right_inv {α : Sort u_1} {β : Sort u_2} (self : α β) :
    Function.RightInverse self.invFun self.toFun

    α ≃ β is the type of functions from α → β with a two-sided inverse.

    Equations
    Instances For
      def EquivLike.toEquiv {α : Sort u} {β : Sort v} {F : Sort u_1} [EquivLike F α β] (f : F) :
      α β

      Turn an element of a type F satisfying EquivLike F α β into an actual Equiv. This is declared as the default coercion from F to α ≃ β.

      Equations
      • f = { toFun := f, invFun := EquivLike.inv f, left_inv := , right_inv := }
      Instances For
        instance instCoeTCEquivOfEquivLike {α : Sort u} {β : Sort v} {F : Sort u_1} [EquivLike F α β] :
        CoeTC F (α β)

        Any type satisfying EquivLike can be cast into Equiv via EquivLike.toEquiv.

        Equations
        • instCoeTCEquivOfEquivLike = { coe := EquivLike.toEquiv }
        @[reducible, inline]
        abbrev Equiv.Perm (α : Sort u_1) :
        Sort (max 1 u_1)

        Perm α is the type of bijections from α to itself.

        Equations
        Instances For
          instance Equiv.instEquivLike {α : Sort u} {β : Sort v} :
          EquivLike (α β) α β
          Equations
          • Equiv.instEquivLike = { coe := Equiv.toFun, inv := Equiv.invFun, left_inv := , right_inv := , coe_injective' := }
          instance Equiv.instFunLike {α : Sort u} {β : Sort v} :
          FunLike (α β) α β

          Helper instance when inference gets stuck on following the normal chain EquivLikeFunLike.

          TODO: this instance doesn't appear to be necessary: remove it (after benchmarking?)

          Equations
          • Equiv.instFunLike = { coe := Equiv.toFun, coe_injective' := }
          @[simp]
          theorem EquivLike.coe_coe {α : Sort u} {β : Sort v} {F : Sort u_1} [EquivLike F α β] (e : F) :
          e = e
          @[simp]
          theorem Equiv.coe_fn_mk {α : Sort u} {β : Sort v} (f : αβ) (g : βα) (l : Function.LeftInverse g f) (r : Function.RightInverse g f) :
          { toFun := f, invFun := g, left_inv := l, right_inv := r } = f
          theorem Equiv.coe_fn_injective {α : Sort u} {β : Sort v} :
          Function.Injective fun (e : α β) => e

          The map (r ≃ s) → (r → s) is injective.

          theorem Equiv.coe_inj {α : Sort u} {β : Sort v} {e₁ : α β} {e₂ : α β} :
          e₁ = e₂ e₁ = e₂
          theorem Equiv.ext_iff {α : Sort u} {β : Sort v} {f : α β} {g : α β} :
          f = g ∀ (x : α), f x = g x
          theorem Equiv.ext {α : Sort u} {β : Sort v} {f : α β} {g : α β} (H : ∀ (x : α), f x = g x) :
          f = g
          theorem Equiv.congr_arg {α : Sort u} {β : Sort v} {f : α β} {x : α} {x' : α} :
          x = x'f x = f x'
          theorem Equiv.congr_fun {α : Sort u} {β : Sort v} {f : α β} {g : α β} (h : f = g) (x : α) :
          f x = g x
          theorem Equiv.Perm.ext_iff {α : Sort u} {σ : Equiv.Perm α} {τ : Equiv.Perm α} :
          σ = τ ∀ (x : α), σ x = τ x
          theorem Equiv.Perm.ext {α : Sort u} {σ : Equiv.Perm α} {τ : Equiv.Perm α} (H : ∀ (x : α), σ x = τ x) :
          σ = τ
          theorem Equiv.Perm.congr_arg {α : Sort u} {f : Equiv.Perm α} {x : α} {x' : α} :
          x = x'f x = f x'
          theorem Equiv.Perm.congr_fun {α : Sort u} {f : Equiv.Perm α} {g : Equiv.Perm α} (h : f = g) (x : α) :
          f x = g x
          def Equiv.refl (α : Sort u_1) :
          α α

          Any type is equivalent to itself.

          Equations
          • Equiv.refl α = { toFun := id, invFun := id, left_inv := , right_inv := }
          Instances For
            instance Equiv.inhabited' {α : Sort u} :
            Inhabited (α α)
            Equations
            def Equiv.symm {α : Sort u} {β : Sort v} (e : α β) :
            β α

            Inverse of an equivalence e : α ≃ β.

            Equations
            • e.symm = { toFun := e.invFun, invFun := e.toFun, left_inv := , right_inv := }
            Instances For
              def Equiv.Simps.symm_apply {α : Sort u} {β : Sort v} (e : α β) :
              βα

              See Note [custom simps projection]

              Equations
              Instances For
                theorem Equiv.left_inv' {α : Sort u} {β : Sort v} (e : α β) :
                Function.LeftInverse e.symm e
                theorem Equiv.right_inv' {α : Sort u} {β : Sort v} (e : α β) :
                Function.RightInverse e.symm e
                def Equiv.trans {α : Sort u} {β : Sort v} {γ : Sort w} (e₁ : α β) (e₂ : β γ) :
                α γ

                Composition of equivalences e₁ : α ≃ β and e₂ : β ≃ γ.

                Equations
                • e₁.trans e₂ = { toFun := e₂ e₁, invFun := e₁.symm e₂.symm, left_inv := , right_inv := }
                Instances For
                  @[simp]
                  theorem Equiv.instTrans_trans :
                  ∀ {a : Sort u_2} {b : Sort u_1} {c : Sort u_3} (e₁ : a b) (e₂ : b c), Trans.trans e₁ e₂ = e₁.trans e₂
                  Equations
                  @[simp]
                  theorem Equiv.toFun_as_coe {α : Sort u} {β : Sort v} (e : α β) :
                  e.toFun = e
                  @[simp]
                  theorem Equiv.invFun_as_coe {α : Sort u} {β : Sort v} (e : α β) :
                  e.invFun = e.symm
                  theorem Equiv.injective {α : Sort u} {β : Sort v} (e : α β) :
                  theorem Equiv.surjective {α : Sort u} {β : Sort v} (e : α β) :
                  theorem Equiv.bijective {α : Sort u} {β : Sort v} (e : α β) :
                  theorem Equiv.subsingleton {α : Sort u} {β : Sort v} (e : α β) [Subsingleton β] :
                  theorem Equiv.subsingleton.symm {α : Sort u} {β : Sort v} (e : α β) [Subsingleton α] :
                  theorem Equiv.subsingleton_congr {α : Sort u} {β : Sort v} (e : α β) :
                  instance Equiv.equiv_subsingleton_cod {α : Sort u} {β : Sort v} [Subsingleton β] :
                  Equations
                  • =
                  instance Equiv.equiv_subsingleton_dom {α : Sort u} {β : Sort v} [Subsingleton α] :
                  Equations
                  • =
                  instance Equiv.permUnique {α : Sort u} [Subsingleton α] :
                  Equations
                  def Equiv.decidableEq {α : Sort u} {β : Sort v} (e : α β) [DecidableEq β] :

                  Transfer DecidableEq across an equivalence.

                  Equations
                  • e.decidableEq = .decidableEq
                  Instances For
                    theorem Equiv.nonempty_congr {α : Sort u} {β : Sort v} (e : α β) :
                    theorem Equiv.nonempty {α : Sort u} {β : Sort v} (e : α β) [Nonempty β] :
                    def Equiv.inhabited {α : Sort u} {β : Sort v} [Inhabited β] (e : α β) :

                    If α ≃ β and β is inhabited, then so is α.

                    Equations
                    • e.inhabited = { default := e.symm default }
                    Instances For
                      def Equiv.unique {α : Sort u} {β : Sort v} [Unique β] (e : α β) :

                      If α ≃ β and β is a singleton type, then so is α.

                      Equations
                      Instances For
                        def Equiv.cast {α : Sort u_1} {β : Sort u_1} (h : α = β) :
                        α β

                        Equivalence between equal types.

                        Equations
                        Instances For
                          @[simp]
                          theorem Equiv.coe_fn_symm_mk {α : Sort u} {β : Sort v} (f : αβ) (g : βα) (l : Function.LeftInverse g f) (r : Function.RightInverse g f) :
                          { toFun := f, invFun := g, left_inv := l, right_inv := r }.symm = g
                          @[simp]
                          theorem Equiv.coe_refl {α : Sort u} :
                          (Equiv.refl α) = id
                          theorem Equiv.Perm.coe_subsingleton {α : Type u_1} [Subsingleton α] (e : Equiv.Perm α) :
                          e = id

                          This cannot be a simp lemmas as it incorrectly matches against e : α ≃ synonym α, when synonym α is semireducible. This makes a mess of Multiplicative.ofAdd etc.

                          @[simp]
                          theorem Equiv.refl_apply {α : Sort u} (x : α) :
                          (Equiv.refl α) x = x
                          @[simp]
                          theorem Equiv.coe_trans {α : Sort u} {β : Sort v} {γ : Sort w} (f : α β) (g : β γ) :
                          (f.trans g) = g f
                          @[simp]
                          theorem Equiv.trans_apply {α : Sort u} {β : Sort v} {γ : Sort w} (f : α β) (g : β γ) (a : α) :
                          (f.trans g) a = g (f a)
                          @[simp]
                          theorem Equiv.apply_symm_apply {α : Sort u} {β : Sort v} (e : α β) (x : β) :
                          e (e.symm x) = x
                          @[simp]
                          theorem Equiv.symm_apply_apply {α : Sort u} {β : Sort v} (e : α β) (x : α) :
                          e.symm (e x) = x
                          @[simp]
                          theorem Equiv.symm_comp_self {α : Sort u} {β : Sort v} (e : α β) :
                          e.symm e = id
                          @[simp]
                          theorem Equiv.self_comp_symm {α : Sort u} {β : Sort v} (e : α β) :
                          e e.symm = id
                          @[simp]
                          theorem EquivLike.apply_coe_symm_apply {α : Sort u} {β : Sort v} {F : Sort u_1} [EquivLike F α β] (e : F) (x : β) :
                          e ((↑e).symm x) = x
                          @[simp]
                          theorem EquivLike.coe_symm_apply_apply {α : Sort u} {β : Sort v} {F : Sort u_1} [EquivLike F α β] (e : F) (x : α) :
                          (↑e).symm (e x) = x
                          @[simp]
                          theorem EquivLike.coe_symm_comp_self {α : Sort u} {β : Sort v} {F : Sort u_1} [EquivLike F α β] (e : F) :
                          (↑e).symm e = id
                          @[simp]
                          theorem EquivLike.self_comp_coe_symm {α : Sort u} {β : Sort v} {F : Sort u_1} [EquivLike F α β] (e : F) :
                          e (↑e).symm = id
                          @[simp]
                          theorem Equiv.symm_trans_apply {α : Sort u} {β : Sort v} {γ : Sort w} (f : α β) (g : β γ) (a : γ) :
                          (f.trans g).symm a = f.symm (g.symm a)
                          theorem Equiv.symm_symm_apply {α : Sort u} {β : Sort v} (f : α β) (b : α) :
                          f.symm.symm b = f b
                          theorem Equiv.apply_eq_iff_eq {α : Sort u} {β : Sort v} (f : α β) {x : α} {y : α} :
                          f x = f y x = y
                          theorem Equiv.apply_eq_iff_eq_symm_apply {α : Sort u} {β : Sort v} {x : α} {y : β} (f : α β) :
                          f x = y x = f.symm y
                          @[simp]
                          theorem Equiv.cast_apply {α : Sort u_1} {β : Sort u_1} (h : α = β) (x : α) :
                          (Equiv.cast h) x = cast h x
                          @[simp]
                          theorem Equiv.cast_symm {α : Sort u_1} {β : Sort u_1} (h : α = β) :
                          (Equiv.cast h).symm = Equiv.cast
                          @[simp]
                          theorem Equiv.cast_refl {α : Sort u_1} (h : optParam (α = α) ) :
                          @[simp]
                          theorem Equiv.cast_trans {α : Sort u_1} {β : Sort u_1} {γ : Sort u_1} (h : α = β) (h2 : β = γ) :
                          (Equiv.cast h).trans (Equiv.cast h2) = Equiv.cast
                          theorem Equiv.cast_eq_iff_heq {α : Sort u_1} {β : Sort u_1} (h : α = β) {a : α} {b : β} :
                          (Equiv.cast h) a = b HEq a b
                          theorem Equiv.symm_apply_eq {α : Sort u_1} {β : Sort u_2} (e : α β) {x : β} {y : α} :
                          e.symm x = y x = e y
                          theorem Equiv.eq_symm_apply {α : Sort u_1} {β : Sort u_2} (e : α β) {x : β} {y : α} :
                          y = e.symm x e y = x
                          @[simp]
                          theorem Equiv.symm_symm {α : Sort u} {β : Sort v} (e : α β) :
                          e.symm.symm = e
                          theorem Equiv.symm_bijective {α : Sort u} {β : Sort v} :
                          @[simp]
                          theorem Equiv.trans_refl {α : Sort u} {β : Sort v} (e : α β) :
                          e.trans (Equiv.refl β) = e
                          @[simp]
                          theorem Equiv.refl_symm {α : Sort u} :
                          (Equiv.refl α).symm = Equiv.refl α
                          @[simp]
                          theorem Equiv.refl_trans {α : Sort u} {β : Sort v} (e : α β) :
                          (Equiv.refl α).trans e = e
                          @[simp]
                          theorem Equiv.symm_trans_self {α : Sort u} {β : Sort v} (e : α β) :
                          e.symm.trans e = Equiv.refl β
                          @[simp]
                          theorem Equiv.self_trans_symm {α : Sort u} {β : Sort v} (e : α β) :
                          e.trans e.symm = Equiv.refl α
                          theorem Equiv.trans_assoc {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} (ab : α β) (bc : β γ) (cd : γ δ) :
                          (ab.trans bc).trans cd = ab.trans (bc.trans cd)
                          theorem Equiv.leftInverse_symm {α : Sort u} {β : Sort v} (f : α β) :
                          Function.LeftInverse f.symm f
                          theorem Equiv.rightInverse_symm {α : Sort u} {β : Sort v} (f : α β) :
                          Function.RightInverse f.symm f
                          theorem Equiv.injective_comp {α : Sort u} {β : Sort v} {γ : Sort w} (e : α β) (f : βγ) :
                          theorem Equiv.comp_injective {α : Sort u} {β : Sort v} {γ : Sort w} (f : αβ) (e : β γ) :
                          theorem Equiv.surjective_comp {α : Sort u} {β : Sort v} {γ : Sort w} (e : α β) (f : βγ) :
                          theorem Equiv.comp_surjective {α : Sort u} {β : Sort v} {γ : Sort w} (f : αβ) (e : β γ) :
                          theorem Equiv.bijective_comp {α : Sort u} {β : Sort v} {γ : Sort w} (e : α β) (f : βγ) :
                          theorem Equiv.comp_bijective {α : Sort u} {β : Sort v} {γ : Sort w} (f : αβ) (e : β γ) :
                          def Equiv.equivCongr {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} (ab : α β) (cd : γ δ) :
                          α γ (β δ)

                          If α is equivalent to β and γ is equivalent to δ, then the type of equivalences α ≃ γ is equivalent to the type of equivalences β ≃ δ.

                          Equations
                          • ab.equivCongr cd = { toFun := fun (ac : α γ) => (ab.symm.trans ac).trans cd, invFun := fun (bd : β δ) => ab.trans (bd.trans cd.symm), left_inv := , right_inv := }
                          Instances For
                            @[simp]
                            theorem Equiv.equivCongr_refl {α : Sort u_1} {β : Sort u_2} :
                            (Equiv.refl α).equivCongr (Equiv.refl β) = Equiv.refl (α β)
                            @[simp]
                            theorem Equiv.equivCongr_symm {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} (ab : α β) (cd : γ δ) :
                            (ab.equivCongr cd).symm = ab.symm.equivCongr cd.symm
                            @[simp]
                            theorem Equiv.equivCongr_trans {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} {ε : Sort u_2} {ζ : Sort u_3} (ab : α β) (de : δ ε) (bc : β γ) (ef : ε ζ) :
                            (ab.equivCongr de).trans (bc.equivCongr ef) = (ab.trans bc).equivCongr (de.trans ef)
                            @[simp]
                            theorem Equiv.equivCongr_refl_left {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (bg : β γ) (e : α β) :
                            ((Equiv.refl α).equivCongr bg) e = e.trans bg
                            @[simp]
                            theorem Equiv.equivCongr_refl_right {α : Sort u_1} {β : Sort u_2} (ab : α β) (e : α β) :
                            (ab.equivCongr (Equiv.refl β)) e = ab.symm.trans e
                            @[simp]
                            theorem Equiv.equivCongr_apply_apply {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} (ab : α β) (cd : γ δ) (e : α γ) (x : β) :
                            ((ab.equivCongr cd) e) x = cd (e (ab.symm x))
                            def Equiv.permCongr {α' : Type u_1} {β' : Type u_2} (e : α' β') :

                            If α is equivalent to β, then Perm α is equivalent to Perm β.

                            Equations
                            • e.permCongr = e.equivCongr e
                            Instances For
                              theorem Equiv.permCongr_def {α' : Type u_1} {β' : Type u_2} (e : α' β') (p : Equiv.Perm α') :
                              e.permCongr p = (e.symm.trans p).trans e
                              @[simp]
                              theorem Equiv.permCongr_refl {α' : Type u_1} {β' : Type u_2} (e : α' β') :
                              e.permCongr (Equiv.refl α') = Equiv.refl β'
                              @[simp]
                              theorem Equiv.permCongr_symm {α' : Type u_1} {β' : Type u_2} (e : α' β') :
                              e.permCongr.symm = e.symm.permCongr
                              @[simp]
                              theorem Equiv.permCongr_apply {α' : Type u_1} {β' : Type u_2} (e : α' β') (p : Equiv.Perm α') (x : β') :
                              (e.permCongr p) x = e (p (e.symm x))
                              theorem Equiv.permCongr_symm_apply {α' : Type u_1} {β' : Type u_2} (e : α' β') (p : Equiv.Perm β') (x : α') :
                              (e.permCongr.symm p) x = e.symm (p (e x))
                              theorem Equiv.permCongr_trans {α' : Type u_1} {β' : Type u_2} (e : α' β') (p : Equiv.Perm α') (p' : Equiv.Perm α') :
                              Equiv.trans (e.permCongr p) (e.permCongr p') = e.permCongr (Equiv.trans p p')
                              def Equiv.equivOfIsEmpty (α : Sort u_1) (β : Sort u_2) [IsEmpty α] [IsEmpty β] :
                              α β

                              Two empty types are equivalent.

                              Equations
                              Instances For
                                def Equiv.equivEmpty (α : Sort u) [IsEmpty α] :

                                If α is an empty type, then it is equivalent to the Empty type.

                                Equations
                                Instances For

                                  If α is an empty type, then it is equivalent to the PEmpty type in any universe.

                                  Equations
                                  Instances For

                                    α is equivalent to an empty type iff α is empty.

                                    Equations
                                    Instances For

                                      The Sort of proofs of a false proposition is equivalent to PEmpty.

                                      Equations
                                      Instances For
                                        def Equiv.equivOfUnique (α : Sort u) (β : Sort v) [Unique α] [Unique β] :
                                        α β

                                        If both α and β have a unique element, then α ≃ β.

                                        Equations
                                        • Equiv.equivOfUnique α β = { toFun := default, invFun := default, left_inv := , right_inv := }
                                        Instances For
                                          def Equiv.equivPUnit (α : Sort u) [Unique α] :

                                          If α has a unique element, then it is equivalent to any PUnit.

                                          Equations
                                          Instances For
                                            def Equiv.propEquivPUnit {p : Prop} (h : p) :

                                            The Sort of proofs of a true proposition is equivalent to PUnit.

                                            Equations
                                            Instances For
                                              @[simp]
                                              theorem Equiv.ulift_apply {α : Type v} :
                                              Equiv.ulift = ULift.down
                                              def Equiv.ulift {α : Type v} :

                                              ULift α is equivalent to α.

                                              Equations
                                              • Equiv.ulift = { toFun := ULift.down, invFun := ULift.up, left_inv := , right_inv := }
                                              Instances For
                                                @[simp]
                                                theorem Equiv.plift_apply {α : Sort u} :
                                                Equiv.plift = PLift.down
                                                def Equiv.plift {α : Sort u} :
                                                PLift α α

                                                PLift α is equivalent to α.

                                                Equations
                                                • Equiv.plift = { toFun := PLift.down, invFun := PLift.up, left_inv := , right_inv := }
                                                Instances For
                                                  def Equiv.ofIff {P : Prop} {Q : Prop} (h : P Q) :
                                                  P Q

                                                  equivalence of propositions is the same as iff

                                                  Equations
                                                  • Equiv.ofIff h = { toFun := , invFun := , left_inv := , right_inv := }
                                                  Instances For
                                                    @[simp]
                                                    theorem Equiv.arrowCongr_apply {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} (e₁ : α₁ α₂) (e₂ : β₁ β₂) (f : α₁β₁) :
                                                    ∀ (a : α₂), (e₁.arrowCongr e₂) f a = (e₂ f e₁.symm) a
                                                    def Equiv.arrowCongr {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} (e₁ : α₁ α₂) (e₂ : β₁ β₂) :
                                                    (α₁β₁) (α₂β₂)

                                                    If α₁ is equivalent to α₂ and β₁ is equivalent to β₂, then the type of maps α₁ → β₁ is equivalent to the type of maps α₂ → β₂.

                                                    Equations
                                                    • e₁.arrowCongr e₂ = { toFun := fun (f : α₁β₁) => e₂ f e₁.symm, invFun := fun (f : α₂β₂) => e₂.symm f e₁, left_inv := , right_inv := }
                                                    Instances For
                                                      theorem Equiv.arrowCongr_comp {α₁ : Sort u_1} {β₁ : Sort u_2} {γ₁ : Sort u_3} {α₂ : Sort u_4} {β₂ : Sort u_5} {γ₂ : Sort u_6} (ea : α₁ α₂) (eb : β₁ β₂) (ec : γ₁ γ₂) (f : α₁β₁) (g : β₁γ₁) :
                                                      (ea.arrowCongr ec) (g f) = (eb.arrowCongr ec) g (ea.arrowCongr eb) f
                                                      @[simp]
                                                      theorem Equiv.arrowCongr_refl {α : Sort u_1} {β : Sort u_2} :
                                                      (Equiv.refl α).arrowCongr (Equiv.refl β) = Equiv.refl (αβ)
                                                      @[simp]
                                                      theorem Equiv.arrowCongr_trans {α₁ : Sort u_1} {α₂ : Sort u_2} {α₃ : Sort u_3} {β₁ : Sort u_4} {β₂ : Sort u_5} {β₃ : Sort u_6} (e₁ : α₁ α₂) (e₁' : β₁ β₂) (e₂ : α₂ α₃) (e₂' : β₂ β₃) :
                                                      (e₁.trans e₂).arrowCongr (e₁'.trans e₂') = (e₁.arrowCongr e₁').trans (e₂.arrowCongr e₂')
                                                      @[simp]
                                                      theorem Equiv.arrowCongr_symm {α₁ : Sort u_1} {α₂ : Sort u_2} {β₁ : Sort u_3} {β₂ : Sort u_4} (e₁ : α₁ α₂) (e₂ : β₁ β₂) :
                                                      (e₁.arrowCongr e₂).symm = e₁.symm.arrowCongr e₂.symm
                                                      @[simp]
                                                      theorem Equiv.arrowCongr'_apply {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (hα : α₁ α₂) (hβ : β₁ β₂) (f : α₁β₁) :
                                                      ∀ (a : α₂), (.arrowCongr' ) f a = (f (.symm a))
                                                      def Equiv.arrowCongr' {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (hα : α₁ α₂) (hβ : β₁ β₂) :
                                                      (α₁β₁) (α₂β₂)

                                                      A version of Equiv.arrowCongr in Type, rather than Sort.

                                                      The equiv_rw tactic is not able to use the default Sort level Equiv.arrowCongr, because Lean's universe rules will not unify ?l_1 with imax (1 ?m_1).

                                                      Equations
                                                      • .arrowCongr' = .arrowCongr
                                                      Instances For
                                                        @[simp]
                                                        theorem Equiv.arrowCongr'_refl {α : Type u_1} {β : Type u_2} :
                                                        (Equiv.refl α).arrowCongr' (Equiv.refl β) = Equiv.refl (αβ)
                                                        @[simp]
                                                        theorem Equiv.arrowCongr'_trans {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {α₃ : Type u_5} {β₃ : Type u_6} (e₁ : α₁ α₂) (e₁' : β₁ β₂) (e₂ : α₂ α₃) (e₂' : β₂ β₃) :
                                                        (e₁.trans e₂).arrowCongr' (e₁'.trans e₂') = (e₁.arrowCongr' e₁').trans (e₂.arrowCongr' e₂')
                                                        @[simp]
                                                        theorem Equiv.arrowCongr'_symm {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ α₂) (e₂ : β₁ β₂) :
                                                        (e₁.arrowCongr' e₂).symm = e₁.symm.arrowCongr' e₂.symm
                                                        @[simp]
                                                        theorem Equiv.conj_apply {α : Sort u} {β : Sort v} (e : α β) (f : αα) :
                                                        ∀ (a : β), e.conj f a = e (f (e.symm a))
                                                        def Equiv.conj {α : Sort u} {β : Sort v} (e : α β) :
                                                        (αα) (ββ)

                                                        Conjugate a map f : α → α by an equivalence α ≃ β.

                                                        Equations
                                                        • e.conj = e.arrowCongr e
                                                        Instances For
                                                          @[simp]
                                                          theorem Equiv.conj_refl {α : Sort u} :
                                                          (Equiv.refl α).conj = Equiv.refl (αα)
                                                          @[simp]
                                                          theorem Equiv.conj_symm {α : Sort u} {β : Sort v} (e : α β) :
                                                          e.conj.symm = e.symm.conj
                                                          @[simp]
                                                          theorem Equiv.conj_trans {α : Sort u} {β : Sort v} {γ : Sort w} (e₁ : α β) (e₂ : β γ) :
                                                          (e₁.trans e₂).conj = e₁.conj.trans e₂.conj
                                                          theorem Equiv.conj_comp {α : Sort u} {β : Sort v} (e : α β) (f₁ : αα) (f₂ : αα) :
                                                          e.conj (f₁ f₂) = e.conj f₁ e.conj f₂
                                                          theorem Equiv.eq_comp_symm {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e : α β) (f : βγ) (g : αγ) :
                                                          f = g e.symm f e = g
                                                          theorem Equiv.comp_symm_eq {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e : α β) (f : βγ) (g : αγ) :
                                                          g e.symm = f g = f e
                                                          theorem Equiv.eq_symm_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e : α β) (f : γα) (g : γβ) :
                                                          f = e.symm g e f = g
                                                          theorem Equiv.symm_comp_eq {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e : α β) (f : γα) (g : γβ) :
                                                          e.symm g = f g = e f
                                                          theorem Equiv.trans_eq_refl_iff_eq_symm {α : Sort u} {β : Sort v} {f : α β} {g : β α} :
                                                          f.trans g = Equiv.refl α f = g.symm
                                                          theorem Equiv.trans_eq_refl_iff_symm_eq {α : Sort u} {β : Sort v} {f : α β} {g : β α} :
                                                          f.trans g = Equiv.refl α f.symm = g
                                                          theorem Equiv.eq_symm_iff_trans_eq_refl {α : Sort u} {β : Sort v} {f : α β} {g : β α} :
                                                          f = g.symm f.trans g = Equiv.refl α
                                                          theorem Equiv.symm_eq_iff_trans_eq_refl {α : Sort u} {β : Sort v} {f : α β} {g : β α} :
                                                          f.symm = g f.trans g = Equiv.refl α

                                                          PUnit sorts in any two universes are equivalent.

                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            noncomputable def Equiv.propEquivBool :

                                                            Prop is noncomputably equivalent to Bool.

                                                            Equations
                                                            Instances For

                                                              The sort of maps to PUnit.{v} is equivalent to PUnit.{w}.

                                                              Equations
                                                              Instances For
                                                                @[simp]
                                                                theorem Equiv.piUnique_apply {α : Sort u} [Unique α] (β : αSort u_1) :
                                                                (Equiv.piUnique β) = fun (f : (i : α) → β i) => f default
                                                                @[simp]
                                                                theorem Equiv.piUnique_symm_apply {α : Sort u} [Unique α] (β : αSort u_1) :
                                                                (Equiv.piUnique β).symm = uniqueElim
                                                                def Equiv.piUnique {α : Sort u} [Unique α] (β : αSort u_1) :
                                                                ((i : α) → β i) β default

                                                                The equivalence (∀ i, β i) ≃ β ⋆ when the domain of β only contains

                                                                Equations
                                                                • Equiv.piUnique β = { toFun := fun (f : (i : α) → β i) => f default, invFun := uniqueElim, left_inv := , right_inv := }
                                                                Instances For
                                                                  @[simp]
                                                                  theorem Equiv.funUnique_symm_apply (α : Sort u) (β : Sort u_1) [Unique α] :
                                                                  (Equiv.funUnique α β).symm = uniqueElim
                                                                  @[simp]
                                                                  theorem Equiv.funUnique_apply (α : Sort u) (β : Sort u_1) [Unique α] :
                                                                  (Equiv.funUnique α β) = fun (f : αβ) => f default
                                                                  def Equiv.funUnique (α : Sort u) (β : Sort u_1) [Unique α] :
                                                                  (αβ) β

                                                                  If α has a unique term, then the type of function α → β is equivalent to β.

                                                                  Equations
                                                                  Instances For
                                                                    def Equiv.punitArrowEquiv (α : Sort u_1) :
                                                                    (PUnit.{u}α) α

                                                                    The sort of maps from PUnit is equivalent to the codomain.

                                                                    Equations
                                                                    Instances For
                                                                      def Equiv.trueArrowEquiv (α : Sort u_1) :
                                                                      (Trueα) α

                                                                      The sort of maps from True is equivalent to the codomain.

                                                                      Equations
                                                                      Instances For
                                                                        def Equiv.arrowPUnitOfIsEmpty (α : Sort u_1) (β : Sort u_2) [IsEmpty α] :
                                                                        (αβ) PUnit.{u}

                                                                        The sort of maps from a type that IsEmpty is equivalent to PUnit.

                                                                        Equations
                                                                        Instances For

                                                                          The sort of maps from Empty is equivalent to PUnit.

                                                                          Equations
                                                                          Instances For

                                                                            The sort of maps from PEmpty is equivalent to PUnit.

                                                                            Equations
                                                                            Instances For

                                                                              The sort of maps from False is equivalent to PUnit.

                                                                              Equations
                                                                              Instances For
                                                                                @[simp]
                                                                                theorem Equiv.psigmaEquivSigma_apply {α : Type u_2} (β : αType u_1) (a : (i : α) ×' β i) :
                                                                                (Equiv.psigmaEquivSigma β) a = a.fst, a.snd
                                                                                @[simp]
                                                                                theorem Equiv.psigmaEquivSigma_symm_apply {α : Type u_2} (β : αType u_1) (a : (i : α) × β i) :
                                                                                (Equiv.psigmaEquivSigma β).symm a = a.fst, a.snd
                                                                                def Equiv.psigmaEquivSigma {α : Type u_2} (β : αType u_1) :
                                                                                (i : α) ×' β i (i : α) × β i

                                                                                A PSigma-type is equivalent to the corresponding Sigma-type.

                                                                                Equations
                                                                                • Equiv.psigmaEquivSigma β = { toFun := fun (a : (i : α) ×' β i) => a.fst, a.snd, invFun := fun (a : (i : α) × β i) => a.fst, a.snd, left_inv := , right_inv := }
                                                                                Instances For
                                                                                  @[simp]
                                                                                  theorem Equiv.psigmaEquivSigmaPLift_apply {α : Sort u_2} (β : αSort u_1) (a : (i : α) ×' β i) :
                                                                                  (Equiv.psigmaEquivSigmaPLift β) a = { down := a.fst }, { down := a.snd }
                                                                                  @[simp]
                                                                                  theorem Equiv.psigmaEquivSigmaPLift_symm_apply {α : Sort u_2} (β : αSort u_1) (a : (i : PLift α) × PLift (β i.down)) :
                                                                                  (Equiv.psigmaEquivSigmaPLift β).symm a = a.fst.down, a.snd.down
                                                                                  def Equiv.psigmaEquivSigmaPLift {α : Sort u_2} (β : αSort u_1) :
                                                                                  (i : α) ×' β i (i : PLift α) × PLift (β i.down)

                                                                                  A PSigma-type is equivalent to the corresponding Sigma-type.

                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Instances For
                                                                                    @[simp]
                                                                                    theorem Equiv.psigmaCongrRight_apply {α : Sort u} {β₁ : αSort u_1} {β₂ : αSort u_2} (F : (a : α) → β₁ a β₂ a) (a : (a : α) ×' β₁ a) :
                                                                                    (Equiv.psigmaCongrRight F) a = a.fst, (F a.fst) a.snd
                                                                                    def Equiv.psigmaCongrRight {α : Sort u} {β₁ : αSort u_1} {β₂ : αSort u_2} (F : (a : α) → β₁ a β₂ a) :
                                                                                    (a : α) ×' β₁ a (a : α) ×' β₂ a

                                                                                    A family of equivalences Π a, β₁ a ≃ β₂ a generates an equivalence between Σ' a, β₁ a and Σ' a, β₂ a.

                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    Instances For
                                                                                      theorem Equiv.psigmaCongrRight_trans {α : Sort u_4} {β₁ : αSort u_1} {β₂ : αSort u_2} {β₃ : αSort u_3} (F : (a : α) → β₁ a β₂ a) (G : (a : α) → β₂ a β₃ a) :
                                                                                      (Equiv.psigmaCongrRight F).trans (Equiv.psigmaCongrRight G) = Equiv.psigmaCongrRight fun (a : α) => (F a).trans (G a)
                                                                                      theorem Equiv.psigmaCongrRight_symm {α : Sort u_3} {β₁ : αSort u_1} {β₂ : αSort u_2} (F : (a : α) → β₁ a β₂ a) :
                                                                                      (Equiv.psigmaCongrRight F).symm = Equiv.psigmaCongrRight fun (a : α) => (F a).symm
                                                                                      theorem Equiv.psigmaCongrRight_refl {α : Sort u_2} {β : αSort u_1} :
                                                                                      (Equiv.psigmaCongrRight fun (a : α) => Equiv.refl (β a)) = Equiv.refl ((a : α) ×' β a)
                                                                                      @[simp]
                                                                                      theorem Equiv.sigmaCongrRight_apply {α : Type u_3} {β₁ : αType u_1} {β₂ : αType u_2} (F : (a : α) → β₁ a β₂ a) (a : (a : α) × β₁ a) :
                                                                                      (Equiv.sigmaCongrRight F) a = a.fst, (F a.fst) a.snd
                                                                                      def Equiv.sigmaCongrRight {α : Type u_3} {β₁ : αType u_1} {β₂ : αType u_2} (F : (a : α) → β₁ a β₂ a) :
                                                                                      (a : α) × β₁ a (a : α) × β₂ a

                                                                                      A family of equivalences Π a, β₁ a ≃ β₂ a generates an equivalence between Σ a, β₁ a and Σ a, β₂ a.

                                                                                      Equations
                                                                                      • Equiv.sigmaCongrRight F = { toFun := fun (a : (a : α) × β₁ a) => a.fst, (F a.fst) a.snd, invFun := fun (a : (a : α) × β₂ a) => a.fst, (F a.fst).symm a.snd, left_inv := , right_inv := }
                                                                                      Instances For
                                                                                        theorem Equiv.sigmaCongrRight_trans {α : Type u_4} {β₁ : αType u_1} {β₂ : αType u_2} {β₃ : αType u_3} (F : (a : α) → β₁ a β₂ a) (G : (a : α) → β₂ a β₃ a) :
                                                                                        (Equiv.sigmaCongrRight F).trans (Equiv.sigmaCongrRight G) = Equiv.sigmaCongrRight fun (a : α) => (F a).trans (G a)
                                                                                        theorem Equiv.sigmaCongrRight_symm {α : Type u_3} {β₁ : αType u_1} {β₂ : αType u_2} (F : (a : α) → β₁ a β₂ a) :
                                                                                        (Equiv.sigmaCongrRight F).symm = Equiv.sigmaCongrRight fun (a : α) => (F a).symm
                                                                                        theorem Equiv.sigmaCongrRight_refl {α : Type u_2} {β : αType u_1} :
                                                                                        (Equiv.sigmaCongrRight fun (a : α) => Equiv.refl (β a)) = Equiv.refl ((a : α) × β a)
                                                                                        def Equiv.psigmaEquivSubtype {α : Type v} (P : αProp) :
                                                                                        (i : α) ×' P i Subtype P

                                                                                        A PSigma with Prop fibers is equivalent to the subtype.

                                                                                        Equations
                                                                                        • Equiv.psigmaEquivSubtype P = { toFun := fun (x : (i : α) ×' P i) => x.fst, , invFun := fun (x : Subtype P) => x.val, , left_inv := , right_inv := }
                                                                                        Instances For
                                                                                          def Equiv.sigmaPLiftEquivSubtype {α : Type v} (P : αProp) :
                                                                                          (i : α) × PLift (P i) Subtype P

                                                                                          A Sigma with PLift fibers is equivalent to the subtype.

                                                                                          Equations
                                                                                          Instances For
                                                                                            def Equiv.sigmaULiftPLiftEquivSubtype {α : Type v} (P : αProp) :
                                                                                            (i : α) × ULift.{u_1, 0} (PLift (P i)) Subtype P

                                                                                            A Sigma with fun i ↦ ULift (PLift (P i)) fibers is equivalent to { x // P x }. Variant of sigmaPLiftEquivSubtype.

                                                                                            Equations
                                                                                            Instances For
                                                                                              @[reducible, inline]
                                                                                              abbrev Equiv.Perm.sigmaCongrRight {α : Type u_1} {β : αType u_2} (F : (a : α) → Equiv.Perm (β a)) :
                                                                                              Equiv.Perm ((a : α) × β a)

                                                                                              A family of permutations Π a, Perm (β a) generates a permutation Perm (Σ a, β₁ a).

                                                                                              Equations
                                                                                              Instances For
                                                                                                @[simp]
                                                                                                theorem Equiv.Perm.sigmaCongrRight_trans {α : Type u_1} {β : αType u_2} (F : (a : α) → Equiv.Perm (β a)) (G : (a : α) → Equiv.Perm (β a)) :
                                                                                                @[simp]
                                                                                                theorem Equiv.Perm.sigmaCongrRight_symm {α : Type u_1} {β : αType u_2} (F : (a : α) → Equiv.Perm (β a)) :
                                                                                                @[simp]
                                                                                                theorem Equiv.Perm.sigmaCongrRight_refl {α : Type u_1} {β : αType u_2} :
                                                                                                (Equiv.Perm.sigmaCongrRight fun (a : α) => Equiv.refl (β a)) = Equiv.refl ((a : α) × β a)
                                                                                                @[simp]
                                                                                                theorem Equiv.sigmaCongrLeft_apply {α₁ : Type u_1} {α₂ : Type u_2} {β : α₂Type u_3} (e : α₁ α₂) (a : (a : α₁) × β (e a)) :
                                                                                                e.sigmaCongrLeft a = e a.fst, a.snd
                                                                                                def Equiv.sigmaCongrLeft {α₁ : Type u_1} {α₂ : Type u_2} {β : α₂Type u_3} (e : α₁ α₂) :
                                                                                                (a : α₁) × β (e a) (a : α₂) × β a

                                                                                                An equivalence f : α₁ ≃ α₂ generates an equivalence between Σ a, β (f a) and Σ a, β a.

                                                                                                Equations
                                                                                                • e.sigmaCongrLeft = { toFun := fun (a : (a : α₁) × β (e a)) => e a.fst, a.snd, invFun := fun (a : (a : α₂) × β a) => e.symm a.fst, a.snd, left_inv := , right_inv := }
                                                                                                Instances For
                                                                                                  def Equiv.sigmaCongrLeft' {α₁ : Type u_1} {α₂ : Type u_2} {β : α₁Type u_3} (f : α₁ α₂) :
                                                                                                  (a : α₁) × β a (a : α₂) × β (f.symm a)

                                                                                                  Transporting a sigma type through an equivalence of the base

                                                                                                  Equations
                                                                                                  • f.sigmaCongrLeft' = f.symm.sigmaCongrLeft.symm
                                                                                                  Instances For
                                                                                                    def Equiv.sigmaCongr {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : α₁Type u_3} {β₂ : α₂Type u_4} (f : α₁ α₂) (F : (a : α₁) → β₁ a β₂ (f a)) :
                                                                                                    Sigma β₁ Sigma β₂

                                                                                                    Transporting a sigma type through an equivalence of the base and a family of equivalences of matching fibers

                                                                                                    Equations
                                                                                                    Instances For
                                                                                                      @[simp]
                                                                                                      theorem Equiv.sigmaEquivProd_symm_apply (α : Type u_1) (β : Type u_2) (a : α × β) :
                                                                                                      (Equiv.sigmaEquivProd α β).symm a = a.fst, a.snd
                                                                                                      @[simp]
                                                                                                      theorem Equiv.sigmaEquivProd_apply (α : Type u_1) (β : Type u_2) (a : (_ : α) × β) :
                                                                                                      (Equiv.sigmaEquivProd α β) a = (a.fst, a.snd)
                                                                                                      def Equiv.sigmaEquivProd (α : Type u_1) (β : Type u_2) :
                                                                                                      (_ : α) × β α × β

                                                                                                      Sigma type with a constant fiber is equivalent to the product.

                                                                                                      Equations
                                                                                                      • Equiv.sigmaEquivProd α β = { toFun := fun (a : (_ : α) × β) => (a.fst, a.snd), invFun := fun (a : α × β) => a.fst, a.snd, left_inv := , right_inv := }
                                                                                                      Instances For
                                                                                                        def Equiv.sigmaEquivProdOfEquiv {α : Type u_1} {β : Type u_2} {β₁ : αType u_3} (F : (a : α) → β₁ a β) :
                                                                                                        Sigma β₁ α × β

                                                                                                        If each fiber of a Sigma type is equivalent to a fixed type, then the sigma type is equivalent to the product.

                                                                                                        Equations
                                                                                                        Instances For
                                                                                                          def Equiv.sigmaAssoc {α : Type u_1} {β : αType u_2} (γ : (a : α) → β aType u_3) :
                                                                                                          (ab : (a : α) × β a) × γ ab.fst ab.snd (a : α) × (b : β a) × γ a b

                                                                                                          Dependent product of types is associative up to an equivalence.

                                                                                                          Equations
                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                          Instances For
                                                                                                            theorem Equiv.forall_congr_right {α : Sort u} {β : Sort v} {q : βProp} (e : α β) :
                                                                                                            (∀ (a : α), q (e a)) ∀ (b : β), q b
                                                                                                            theorem Equiv.forall_congr_left {α : Sort u} {β : Sort v} {p : αProp} (e : α β) :
                                                                                                            (∀ (a : α), p a) ∀ (b : β), p (e.symm b)
                                                                                                            @[deprecated Equiv.forall_congr_left]
                                                                                                            theorem Equiv.forall_congr_left' {α : Sort u} {β : Sort v} {p : αProp} (e : α β) :
                                                                                                            (∀ (a : α), p a) ∀ (b : β), p (e.symm b)

                                                                                                            Alias of Equiv.forall_congr_left.

                                                                                                            theorem Equiv.forall_congr {α : Sort u} {β : Sort v} {p : αProp} {q : βProp} (e : α β) (h : ∀ (a : α), p a q (e a)) :
                                                                                                            (∀ (a : α), p a) ∀ (b : β), q b
                                                                                                            theorem Equiv.forall_congr' {α : Sort u} {β : Sort v} {p : αProp} {q : βProp} (e : α β) (h : ∀ (b : β), p (e.symm b) q b) :
                                                                                                            (∀ (a : α), p a) ∀ (b : β), q b
                                                                                                            theorem Equiv.exists_congr_right {α : Sort u} {β : Sort v} {q : βProp} (e : α β) :
                                                                                                            (∃ (a : α), q (e a)) ∃ (b : β), q b
                                                                                                            theorem Equiv.exists_congr_left {α : Sort u} {β : Sort v} {p : αProp} (e : α β) :
                                                                                                            (∃ (a : α), p a) ∃ (b : β), p (e.symm b)
                                                                                                            theorem Equiv.exists_congr {α : Sort u} {β : Sort v} {p : αProp} {q : βProp} (e : α β) (h : ∀ (a : α), p a q (e a)) :
                                                                                                            (∃ (a : α), p a) ∃ (b : β), q b
                                                                                                            theorem Equiv.exists_congr' {α : Sort u} {β : Sort v} {p : αProp} {q : βProp} (e : α β) (h : ∀ (b : β), p (e.symm b) q b) :
                                                                                                            (∃ (a : α), p a) ∃ (b : β), q b
                                                                                                            theorem Equiv.existsUnique_congr_right {α : Sort u} {β : Sort v} {q : βProp} (e : α β) :
                                                                                                            (∃! a : α, q (e a)) ∃! b : β, q b
                                                                                                            theorem Equiv.existsUnique_congr_left {α : Sort u} {β : Sort v} {p : αProp} (e : α β) :
                                                                                                            (∃! a : α, p a) ∃! b : β, p (e.symm b)
                                                                                                            @[deprecated Equiv.existsUnique_congr_right]
                                                                                                            theorem Equiv.exists_unique_congr_left {α : Sort u} {β : Sort v} {q : βProp} (e : α β) :
                                                                                                            (∃! a : α, q (e a)) ∃! b : β, q b

                                                                                                            Alias of Equiv.existsUnique_congr_right.

                                                                                                            @[deprecated Equiv.existsUnique_congr_left]
                                                                                                            theorem Equiv.exists_unique_congr_left' {α : Sort u} {β : Sort v} {p : αProp} (e : α β) :
                                                                                                            (∃! a : α, p a) ∃! b : β, p (e.symm b)

                                                                                                            Alias of Equiv.existsUnique_congr_left.

                                                                                                            theorem Equiv.existsUnique_congr {α : Sort u} {β : Sort v} {p : αProp} {q : βProp} (e : α β) (h : ∀ (a : α), p a q (e a)) :
                                                                                                            (∃! a : α, p a) ∃! b : β, q b
                                                                                                            @[deprecated Equiv.existsUnique_congr]
                                                                                                            theorem Equiv.exists_unique_congr {α : Sort u} {β : Sort v} {p : αProp} {q : βProp} (e : α β) (h : ∀ (a : α), p a q (e a)) :
                                                                                                            (∃! a : α, p a) ∃! b : β, q b

                                                                                                            Alias of Equiv.existsUnique_congr.

                                                                                                            theorem Equiv.existsUnique_congr' {α : Sort u} {β : Sort v} {p : αProp} {q : βProp} (e : α β) (h : ∀ (b : β), p (e.symm b) q b) :
                                                                                                            (∃! a : α, p a) ∃! b : β, q b
                                                                                                            theorem Equiv.forall₂_congr {α₁ : Sort u_1} {α₂ : Sort u_2} {β₁ : Sort u_3} {β₂ : Sort u_4} {p : α₁β₁Prop} {q : α₂β₂Prop} (eα : α₁ α₂) (eβ : β₁ β₂) (h : ∀ {x : α₁} {y : β₁}, p x y q ( x) ( y)) :
                                                                                                            (∀ (x : α₁) (y : β₁), p x y) ∀ (x : α₂) (y : β₂), q x y
                                                                                                            theorem Equiv.forall₂_congr' {α₁ : Sort u_1} {α₂ : Sort u_2} {β₁ : Sort u_3} {β₂ : Sort u_4} {p : α₁β₁Prop} {q : α₂β₂Prop} (eα : α₁ α₂) (eβ : β₁ β₂) (h : ∀ {x : α₂} {y : β₂}, p (.symm x) (.symm y) q x y) :
                                                                                                            (∀ (x : α₁) (y : β₁), p x y) ∀ (x : α₂) (y : β₂), q x y
                                                                                                            theorem Equiv.forall₃_congr {α₁ : Sort u_1} {α₂ : Sort u_2} {β₁ : Sort u_3} {β₂ : Sort u_4} {γ₁ : Sort u_5} {γ₂ : Sort u_6} {p : α₁β₁γ₁Prop} {q : α₂β₂γ₂Prop} (eα : α₁ α₂) (eβ : β₁ β₂) (eγ : γ₁ γ₂) (h : ∀ {x : α₁} {y : β₁} {z : γ₁}, p x y z q ( x) ( y) ( z)) :
                                                                                                            (∀ (x : α₁) (y : β₁) (z : γ₁), p x y z) ∀ (x : α₂) (y : β₂) (z : γ₂), q x y z
                                                                                                            theorem Equiv.forall₃_congr' {α₁ : Sort u_1} {α₂ : Sort u_2} {β₁ : Sort u_3} {β₂ : Sort u_4} {γ₁ : Sort u_5} {γ₂ : Sort u_6} {p : α₁β₁γ₁Prop} {q : α₂β₂γ₂Prop} (eα : α₁ α₂) (eβ : β₁ β₂) (eγ : γ₁ γ₂) (h : ∀ {x : α₂} {y : β₂} {z : γ₂}, p (.symm x) (.symm y) (.symm z) q x y z) :
                                                                                                            (∀ (x : α₁) (y : β₁) (z : γ₁), p x y z) ∀ (x : α₂) (y : β₂) (z : γ₂), q x y z
                                                                                                            @[simp]
                                                                                                            theorem Equiv.ofBijective_apply {α : Sort u} {β : Sort v} (f : αβ) (hf : Function.Bijective f) :
                                                                                                            ∀ (a : α), (Equiv.ofBijective f hf) a = f a
                                                                                                            noncomputable def Equiv.ofBijective {α : Sort u} {β : Sort v} (f : αβ) (hf : Function.Bijective f) :
                                                                                                            α β

                                                                                                            If f is a bijective function, then its domain is equivalent to its codomain.

                                                                                                            Equations
                                                                                                            Instances For
                                                                                                              theorem Equiv.ofBijective_apply_symm_apply {α : Sort u} {β : Sort v} (f : αβ) (hf : Function.Bijective f) (x : β) :
                                                                                                              f ((Equiv.ofBijective f hf).symm x) = x
                                                                                                              @[simp]
                                                                                                              theorem Equiv.ofBijective_symm_apply_apply {α : Sort u} {β : Sort v} (f : αβ) (hf : Function.Bijective f) (x : α) :
                                                                                                              (Equiv.ofBijective f hf).symm (f x) = x
                                                                                                              def Quot.congr {α : Sort u} {β : Sort v} {ra : ααProp} {rb : ββProp} (e : α β) (eq : ∀ (a₁ a₂ : α), ra a₁ a₂ rb (e a₁) (e a₂)) :
                                                                                                              Quot ra Quot rb

                                                                                                              An equivalence e : α ≃ β generates an equivalence between quotient spaces, if ra a₁ a₂ ↔ rb (e a₁) (e a₂).

                                                                                                              Equations
                                                                                                              Instances For
                                                                                                                @[simp]
                                                                                                                theorem Quot.congr_mk {α : Sort u} {β : Sort v} {ra : ααProp} {rb : ββProp} (e : α β) (eq : ∀ (a₁ a₂ : α), ra a₁ a₂ rb (e a₁) (e a₂)) (a : α) :
                                                                                                                (Quot.congr e eq) (Quot.mk ra a) = Quot.mk rb (e a)
                                                                                                                def Quot.congrRight {α : Sort u} {r : ααProp} {r' : ααProp} (eq : ∀ (a₁ a₂ : α), r a₁ a₂ r' a₁ a₂) :

                                                                                                                Quotients are congruent on equivalences under equality of their relation. An alternative is just to use rewriting with eq, but then computational proofs get stuck.

                                                                                                                Equations
                                                                                                                Instances For
                                                                                                                  def Quot.congrLeft {α : Sort u} {β : Sort v} {r : ααProp} (e : α β) :
                                                                                                                  Quot r Quot fun (b b' : β) => r (e.symm b) (e.symm b')

                                                                                                                  An equivalence e : α ≃ β generates an equivalence between the quotient space of α by a relation ra and the quotient space of β by the image of this relation under e.

                                                                                                                  Equations
                                                                                                                  Instances For
                                                                                                                    def Quotient.congr {α : Sort u} {β : Sort v} {ra : Setoid α} {rb : Setoid β} (e : α β) (eq : ∀ (a₁ a₂ : α), ra a₁ a₂ rb (e a₁) (e a₂)) :

                                                                                                                    An equivalence e : α ≃ β generates an equivalence between quotient spaces, if ra a₁ a₂ ↔ rb (e a₁) (e a₂).

                                                                                                                    Equations
                                                                                                                    Instances For
                                                                                                                      @[simp]
                                                                                                                      theorem Quotient.congr_mk {α : Sort u} {β : Sort v} {ra : Setoid α} {rb : Setoid β} (e : α β) (eq : ∀ (a₁ a₂ : α), ra a₁ a₂ rb (e a₁) (e a₂)) (a : α) :
                                                                                                                      (Quotient.congr e eq) a = e a
                                                                                                                      def Quotient.congrRight {α : Sort u} {r : Setoid α} {r' : Setoid α} (eq : ∀ (a₁ a₂ : α), r a₁ a₂ r' a₁ a₂) :

                                                                                                                      Quotients are congruent on equivalences under equality of their relation. An alternative is just to use rewriting with eq, but then computational proofs get stuck.

                                                                                                                      Equations
                                                                                                                      Instances For