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
    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 α ≃ β.

    Instances For
      instance instCoeTCEquiv {α : Sort u} {β : Sort v} {F : Sort u_1} [EquivLike F α β] :
      CoeTC F (α β)

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

      @[reducible]
      def Equiv.Perm (α : Sort u_1) :
      Sort (max 1 u_1)

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

      Instances For
        instance Equiv.instEquivLikeEquiv {α : Sort u} {β : Sort v} :
        EquivLike (α β) α β
        instance Equiv.instFunLikeEquiv {α : Sort u} {β : Sort v} :
        FunLike (α β) α fun x => β

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

        @[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 {α : 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.ext_iff {α : Sort u} {β : Sort v} {f : α β} {g : α β} :
        f = g ∀ (x : α), f x = g 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
        theorem Equiv.Perm.ext_iff {α : Sort u} {σ : Equiv.Perm α} {τ : Equiv.Perm α} :
        σ = τ ∀ (x : α), σ x = τ x
        def Equiv.refl (α : Sort u_1) :
        α α

        Any type is equivalent to itself.

        Instances For
          instance Equiv.inhabited' {α : Sort u} :
          Inhabited (α α)
          def Equiv.symm {α : Sort u} {β : Sort v} (e : α β) :
          β α

          Inverse of an equivalence e : α ≃ β.

          Instances For
            def Equiv.Simps.symm_apply {α : Sort u} {β : Sort v} (e : α β) :
            βα

            See Note [custom simps projection]

            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₂ : β ≃ γ.

              Instances For
                @[simp]
                theorem Equiv.instTransSortSortSortEquivEquivEquiv_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₂
                @[simp]
                theorem Equiv.toFun_as_coe {α : Sort u} {β : Sort v} (e : α β) :
                e.toFun = e
                @[simp]
                theorem Equiv.toFun_as_coe_apply {α : Sort u} {β : Sort v} (e : α β) (x : α) :
                Equiv.toFun e x = e x
                @[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 β] :
                instance Equiv.equiv_subsingleton_dom {α : Sort u} {β : Sort v} [Subsingleton α] :
                def Equiv.decidableEq {α : Sort u} {β : Sort v} (e : α β) [DecidableEq β] :

                Transfer DecidableEq across an equivalence.

                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 α.

                  Instances For
                    def Equiv.unique {α : Sort u} {β : Sort v} [Unique β] (e : α β) :

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

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

                      Equivalence between equal types.

                      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 Equiv.symm_trans_apply {α : Sort u} {β : Sort v} {γ : Sort w} (f : α β) (g : β γ) (a : γ) :
                        (f.trans g).symm a = f.symm (g.symm a)
                        @[simp]
                        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 : (fun x => β) x} (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 : (fun x => α) x} :
                        e.symm x = y x = e y
                        theorem Equiv.eq_symm_apply {α : Sort u_1} {β : Sort u_2} (e : α β) {x : β} {y : (fun x => α) x} :
                        y = e.symm x e y = x
                        @[simp]
                        theorem Equiv.symm_symm {α : Sort u} {β : Sort v} (e : α β) :
                        e.symm.symm = e
                        @[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 β ≃ δ.

                        Instances For
                          @[simp]
                          theorem Equiv.equivCongr_refl {α : Sort u_1} {β : Sort u_2} :
                          @[simp]
                          theorem Equiv.equivCongr_symm {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} (ab : α β) (cd : γ δ) :
                          (Equiv.equivCongr ab cd).symm = Equiv.equivCongr ab.symm 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 : ε ζ) :
                          (Equiv.equivCongr ab de).trans (Equiv.equivCongr bc ef) = Equiv.equivCongr (ab.trans bc) (de.trans ef)
                          @[simp]
                          theorem Equiv.equivCongr_refl_left {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (bg : β γ) (e : α β) :
                          ↑(Equiv.equivCongr (Equiv.refl α) bg) e = e.trans bg
                          @[simp]
                          theorem Equiv.equivCongr_refl_right {α : Sort u_1} {β : Sort u_2} (ab : α β) (e : α β) :
                          ↑(Equiv.equivCongr ab (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 : β) :
                          ↑(↑(Equiv.equivCongr ab 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 β.

                          Instances For
                            theorem Equiv.permCongr_def {α' : Type u_1} {β' : Type u_2} (e : α' β') (p : Equiv.Perm α') :
                            ↑(Equiv.permCongr e) p = (e.symm.trans p).trans e
                            @[simp]
                            theorem Equiv.permCongr_refl {α' : Type u_1} {β' : Type u_2} (e : α' β') :
                            @[simp]
                            theorem Equiv.permCongr_symm {α' : Type u_1} {β' : Type u_2} (e : α' β') :
                            @[simp]
                            theorem Equiv.permCongr_apply {α' : Type u_1} {β' : Type u_2} (e : α' β') (p : Equiv.Perm α') (x : β') :
                            ↑(↑(Equiv.permCongr e) p) x = e (p (e.symm x))
                            theorem Equiv.permCongr_symm_apply {α' : Type u_1} {β' : Type u_2} (e : α' β') (p : Equiv.Perm β') (x : α') :
                            ↑((Equiv.permCongr e).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.permCongr e) p).trans (↑(Equiv.permCongr e) p') = ↑(Equiv.permCongr e) (p.trans p')
                            def Equiv.equivOfIsEmpty (α : Sort u_1) (β : Sort u_2) [IsEmpty α] [IsEmpty β] :
                            α β

                            Two empty types are equivalent.

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

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

                              Instances For

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

                                Instances For

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

                                  Instances For

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

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

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

                                      Instances For
                                        def Equiv.equivPUnit (α : Sort u) [Unique α] :

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

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

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

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

                                            ULift α is equivalent to α.

                                            Instances For
                                              @[simp]
                                              theorem Equiv.plift_apply {α : Sort u} :
                                              Equiv.plift = PLift.down
                                              def Equiv.plift {α : Sort u} :
                                              PLift α α

                                              PLift α is equivalent to α.

                                              Instances For
                                                def Equiv.ofIff {P : Prop} {Q : Prop} (h : P Q) :
                                                P Q

                                                equivalence of propositions is the same as iff

                                                Instances For
                                                  @[simp]
                                                  theorem Equiv.arrowCongr_apply {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} (e₁ : α₁ α₂) (e₂ : β₁ β₂) (f : α₁β₁) :
                                                  ∀ (a : α₂), ↑(Equiv.arrowCongr e₁ 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 α₂ → β₂.

                                                  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 : β₁γ₁) :
                                                    ↑(Equiv.arrowCongr ea ec) (g f) = ↑(Equiv.arrowCongr eb ec) g ↑(Equiv.arrowCongr ea eb) f
                                                    @[simp]
                                                    theorem Equiv.arrowCongr_refl {α : Sort u_1} {β : Sort u_2} :
                                                    @[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₂' : β₂ β₃) :
                                                    Equiv.arrowCongr (e₁.trans e₂) (e₁'.trans e₂') = (Equiv.arrowCongr e₁ e₁').trans (Equiv.arrowCongr e₂ e₂')
                                                    @[simp]
                                                    theorem Equiv.arrowCongr_symm {α₁ : Sort u_1} {α₂ : Sort u_2} {β₁ : Sort u_3} {β₂ : Sort u_4} (e₁ : α₁ α₂) (e₂ : β₁ β₂) :
                                                    (Equiv.arrowCongr e₁ e₂).symm = Equiv.arrowCongr e₁.symm e₂.symm
                                                    @[simp]
                                                    theorem Equiv.arrowCongr'_apply {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (hα : α₁ α₂) (hβ : β₁ β₂) (f : α₁β₁) :
                                                    ∀ (a : α₂), ↑(Equiv.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).

                                                    Instances For
                                                      @[simp]
                                                      theorem Equiv.arrowCongr'_refl {α : Type u_1} {β : Type u_2} :
                                                      @[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₂' : β₂ β₃) :
                                                      Equiv.arrowCongr' (e₁.trans e₂) (e₁'.trans e₂') = (Equiv.arrowCongr' e₁ e₁').trans (Equiv.arrowCongr' e₂ e₂')
                                                      @[simp]
                                                      theorem Equiv.arrowCongr'_symm {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ α₂) (e₂ : β₁ β₂) :
                                                      (Equiv.arrowCongr' e₁ e₂).symm = Equiv.arrowCongr' e₁.symm e₂.symm
                                                      @[simp]
                                                      theorem Equiv.conj_apply {α : Sort u} {β : Sort v} (e : α β) (f : αα) :
                                                      ∀ (a : β), ↑(Equiv.conj e) f a = e (f (e.symm a))
                                                      def Equiv.conj {α : Sort u} {β : Sort v} (e : α β) :
                                                      (αα) (ββ)

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

                                                      Instances For
                                                        @[simp]
                                                        theorem Equiv.conj_refl {α : Sort u} :
                                                        @[simp]
                                                        theorem Equiv.conj_symm {α : Sort u} {β : Sort v} (e : α β) :
                                                        (Equiv.conj e).symm = Equiv.conj e.symm
                                                        @[simp]
                                                        theorem Equiv.conj_trans {α : Sort u} {β : Sort v} {γ : Sort w} (e₁ : α β) (e₂ : β γ) :
                                                        Equiv.conj (e₁.trans e₂) = (Equiv.conj e₁).trans (Equiv.conj e₂)
                                                        theorem Equiv.conj_comp {α : Sort u} {β : Sort v} (e : α β) (f₁ : αα) (f₂ : αα) :
                                                        ↑(Equiv.conj e) (f₁ f₂) = ↑(Equiv.conj e) f₁ ↑(Equiv.conj e) 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

                                                        PUnit sorts in any two universes are equivalent.

                                                        Instances For
                                                          noncomputable def Equiv.propEquivBool :

                                                          Prop is noncomputably equivalent to Bool.

                                                          Instances For

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

                                                            Instances For
                                                              @[simp]
                                                              theorem Equiv.piSubsingleton_symm_apply {α : Sort u} (β : αSort u_1) [Subsingleton α] (a : α) (x : β a) (b : α) :
                                                              (Equiv.piSubsingleton β a).symm x b = cast (_ : β a = β b) x
                                                              @[simp]
                                                              theorem Equiv.piSubsingleton_apply {α : Sort u} (β : αSort u_1) [Subsingleton α] (a : α) (f : (x : α) → β x) :
                                                              def Equiv.piSubsingleton {α : Sort u} (β : αSort u_1) [Subsingleton α] (a : α) :
                                                              ((a' : α) → β a') β a

                                                              If α is Subsingleton and a : α, then the type of dependent functions Π (i : α), β i is equivalent to β a.

                                                              Instances For
                                                                @[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 β.

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

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

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

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

                                                                    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.

                                                                      Instances For

                                                                        The sort of maps from Empty is equivalent to PUnit.

                                                                        Instances For

                                                                          The sort of maps from PEmpty is equivalent to PUnit.

                                                                          Instances For

                                                                            The sort of maps from False is equivalent to PUnit.

                                                                            Instances For
                                                                              @[simp]
                                                                              theorem Equiv.psigmaEquivSigma_symm_apply {α : Type u_2} (β : αType u_1) (a : (i : α) × β i) :
                                                                              (Equiv.psigmaEquivSigma β).symm a = { fst := a.fst, snd := a.snd }
                                                                              @[simp]
                                                                              theorem Equiv.psigmaEquivSigma_apply {α : Type u_2} (β : αType u_1) (a : (i : α) ×' β i) :
                                                                              ↑(Equiv.psigmaEquivSigma β) a = { fst := a.fst, snd := 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.

                                                                              Instances For
                                                                                @[simp]
                                                                                theorem Equiv.psigmaEquivSigmaPLift_symm_apply {α : Sort u_2} (β : αSort u_1) (a : (i : PLift α) × PLift (β i.down)) :
                                                                                (Equiv.psigmaEquivSigmaPLift β).symm a = { fst := a.fst.down, snd := a.snd.down }
                                                                                @[simp]
                                                                                theorem Equiv.psigmaEquivSigmaPLift_apply {α : Sort u_2} (β : αSort u_1) (a : (i : α) ×' β i) :
                                                                                ↑(Equiv.psigmaEquivSigmaPLift β) a = { fst := { down := a.fst }, snd := { down := a.snd } }
                                                                                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.

                                                                                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 = { fst := a.fst, snd := ↑(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.

                                                                                  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) :
                                                                                    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 = { fst := a.fst, snd := ↑(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.

                                                                                    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.

                                                                                      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.

                                                                                        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.

                                                                                          Instances For
                                                                                            @[reducible]
                                                                                            def 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).

                                                                                            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)) :
                                                                                              ↑(Equiv.sigmaCongrLeft e) a = { fst := e a.fst, snd := 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.

                                                                                              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

                                                                                                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

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

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

                                                                                                    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.

                                                                                                      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.

                                                                                                        Instances For
                                                                                                          theorem Equiv.exists_unique_congr {α : Sort u} {β : Sort v} {p : αProp} {q : βProp} (f : α β) (h : ∀ {x : α}, p x q (f x)) :
                                                                                                          (∃! x, p x) ∃! y, q y
                                                                                                          theorem Equiv.exists_unique_congr_left' {α : Sort u} {β : Sort v} {p : αProp} (f : α β) :
                                                                                                          (∃! x, p x) ∃! y, p (f.symm y)
                                                                                                          theorem Equiv.exists_unique_congr_left {α : Sort u} {β : Sort v} {p : βProp} (f : α β) :
                                                                                                          (∃! x, p (f x)) ∃! y, p y
                                                                                                          theorem Equiv.forall_congr {α : Sort u} {β : Sort v} {p : αProp} {q : βProp} (f : α β) (h : ∀ {x : α}, p x q (f x)) :
                                                                                                          ((x : α) → p x) (y : β) → q y
                                                                                                          theorem Equiv.forall_congr' {α : Sort u} {β : Sort v} {p : αProp} {q : βProp} (f : α β) (h : ∀ {x : β}, p (f.symm x) q x) :
                                                                                                          ((x : α) → p x) (y : β) → q 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 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
                                                                                                          theorem Equiv.forall_congr_left' {α : Sort u} {β : Sort v} {p : αProp} (f : α β) :
                                                                                                          ((x : α) → p x) (y : β) → p (f.symm y)
                                                                                                          theorem Equiv.forall_congr_left {α : Sort u} {β : Sort v} {p : βProp} (f : α β) :
                                                                                                          ((x : α) → p (f x)) (y : β) → p y
                                                                                                          theorem Equiv.exists_congr_left {α : Sort u_1} {β : Sort u_2} (f : α β) {p : αProp} :
                                                                                                          (a, p a) b, p (f.symm b)
                                                                                                          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₂).

                                                                                                          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.

                                                                                                            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.

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

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

                                                                                                                Instances For
                                                                                                                  @[simp]
                                                                                                                  theorem Quotient.congr_mk {α : Sort u} {β : Sort v} {ra : Setoid α} {rb : Setoid β} (e : α β) (eq : ∀ (a₁ a₂ : α), Setoid.r a₁ a₂ Setoid.r (e a₁) (e a₂)) (a : α) :
                                                                                                                  ↑(Quotient.congr e eq) (Quotient.mk ra a) = Quotient.mk rb (e a)
                                                                                                                  def Quotient.congrRight {α : Sort u} {r : Setoid α} {r' : Setoid α} (eq : ∀ (a₁ a₂ : α), Setoid.r a₁ a₂ Setoid.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.

                                                                                                                  Instances For