Documentation

Mathlib.Order.RelIso.Basic

Relation homomorphisms, embeddings, isomorphisms #

This file defines relation homomorphisms, embeddings, isomorphisms and order embeddings and isomorphisms.

Main declarations #

Notation #

structure RelHom {α : Type u_5} {β : Type u_6} (r : ααProp) (s : ββProp) :
Type (max u_5 u_6)

A relation homomorphism with respect to a given pair of relations r and s is a function f : α → β such that r a b → s (f a) (f b).

  • toFun : αβ

    The underlying function of a RelHom

  • map_rel' : ∀ {a b : α}, r a bs (self.toFun a) (self.toFun b)

    A RelHom sends related elements to related elements

Instances For
    theorem RelHom.map_rel' {α : Type u_5} {β : Type u_6} {r : ααProp} {s : ββProp} (self : r →r s) {a : α} {b : α} :
    r a bs (self.toFun a) (self.toFun b)

    A RelHom sends related elements to related elements

    A relation homomorphism with respect to a given pair of relations r and s is a function f : α → β such that r a b → s (f a) (f b).

    Equations
    Instances For
      class RelHomClass (F : Type u_5) {α : outParam (Type u_6)} {β : outParam (Type u_7)} (r : outParam (ααProp)) (s : outParam (ββProp)) [FunLike F α β] :

      RelHomClass F r s asserts that F is a type of functions such that all f : F satisfy r a b → s (f a) (f b).

      The relations r and s are outParams since figuring them out from a goal is a higher-order matching problem that Lean usually can't do unaided.

      • map_rel : ∀ (f : F) {a b : α}, r a bs (f a) (f b)

        A RelHomClass sends related elements to related elements

      Instances
        theorem RelHomClass.map_rel {F : Type u_5} {α : outParam (Type u_6)} {β : outParam (Type u_7)} {r : outParam (ααProp)} {s : outParam (ββProp)} :
        ∀ {inst : FunLike F α β} [self : RelHomClass F r s] (f : F) {a b : α}, r a bs (f a) (f b)

        A RelHomClass sends related elements to related elements

        theorem RelHomClass.isIrrefl {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {F : Type u_5} [FunLike F α β] [RelHomClass F r s] (f : F) [IsIrrefl β s] :
        theorem RelHomClass.isAsymm {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {F : Type u_5} [FunLike F α β] [RelHomClass F r s] (f : F) [IsAsymm β s] :
        IsAsymm α r
        theorem RelHomClass.acc {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {F : Type u_5} [FunLike F α β] [RelHomClass F r s] (f : F) (a : α) :
        Acc s (f a)Acc r a
        theorem RelHomClass.wellFounded {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {F : Type u_5} [FunLike F α β] [RelHomClass F r s] (f : F) :
        theorem RelHomClass.isWellFounded {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {F : Type u_5} [FunLike F α β] [RelHomClass F r s] (f : F) [IsWellFounded β s] :
        instance RelHom.instFunLike {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
        FunLike (r →r s) α β
        Equations
        • RelHom.instFunLike = { coe := fun (o : r →r s) => o.toFun, coe_injective' := }
        instance RelHom.instRelHomClass {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
        RelHomClass (r →r s) r s
        Equations
        • =
        theorem RelHom.map_rel {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r →r s) {a : α} {b : α} :
        r a bs (f a) (f b)
        @[simp]
        theorem RelHom.coe_fn_toFun {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r →r s) :
        f.toFun = f
        theorem RelHom.coe_fn_injective {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
        Function.Injective fun (f : r →r s) => f

        The map coe_fn : (r →r s) → (α → β) is injective.

        theorem RelHom.ext_iff {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {f : r →r s} {g : r →r s} :
        f = g ∀ (x : α), f x = g x
        theorem RelHom.ext {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} ⦃f : r →r s ⦃g : r →r s (h : ∀ (x : α), f x = g x) :
        f = g
        @[simp]
        theorem RelHom.id_apply {α : Type u_1} (r : ααProp) (x : α) :
        (RelHom.id r) x = x
        def RelHom.id {α : Type u_1} (r : ααProp) :
        r →r r

        Identity map is a relation homomorphism.

        Equations
        • RelHom.id r = { toFun := fun (x : α) => x, map_rel' := }
        Instances For
          @[simp]
          theorem RelHom.comp_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} (g : s →r t) (f : r →r s) (x : α) :
          (g.comp f) x = g (f x)
          def RelHom.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} (g : s →r t) (f : r →r s) :
          r →r t

          Composition of two relation homomorphisms is a relation homomorphism.

          Equations
          • g.comp f = { toFun := fun (x : α) => g (f x), map_rel' := }
          Instances For
            def RelHom.swap {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r →r s) :

            A relation homomorphism is also a relation homomorphism between dual relations.

            Equations
            • f.swap = { toFun := f, map_rel' := }
            Instances For
              def RelHom.preimage {α : Type u_1} {β : Type u_2} (f : αβ) (s : ββProp) :

              A function is a relation homomorphism from the preimage relation of s to s.

              Equations
              Instances For
                theorem injective_of_increasing {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsTrichotomous α r] [IsIrrefl β s] (f : αβ) (hf : ∀ {x y : α}, r x ys (f x) (f y)) :

                An increasing function is injective

                theorem RelHom.injective_of_increasing {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsTrichotomous α r] [IsIrrefl β s] (f : r →r s) :

                An increasing function is injective

                theorem Function.Surjective.wellFounded_iff {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {f : αβ} (hf : Function.Surjective f) (o : ∀ {a b : α}, r a b s (f a) (f b)) :
                structure RelEmbedding {α : Type u_5} {β : Type u_6} (r : ααProp) (s : ββProp) extends Function.Embedding :
                Type (max u_5 u_6)

                A relation embedding with respect to a given pair of relations r and s is an embedding f : α ↪ β such that r a b ↔ s (f a) (f b).

                • toFun : αβ
                • inj' : Function.Injective self.toFun
                • map_rel_iff' : ∀ {a b : α}, s (self.toEmbedding a) (self.toEmbedding b) r a b

                  Elements are related iff they are related after apply a RelEmbedding

                Instances For
                  theorem RelEmbedding.map_rel_iff' {α : Type u_5} {β : Type u_6} {r : ααProp} {s : ββProp} (self : r ↪r s) {a : α} {b : α} :
                  s (self.toEmbedding a) (self.toEmbedding b) r a b

                  Elements are related iff they are related after apply a RelEmbedding

                  A relation embedding with respect to a given pair of relations r and s is an embedding f : α ↪ β such that r a b ↔ s (f a) (f b).

                  Equations
                  Instances For
                    def Subtype.relEmbedding {X : Type u_5} (r : XXProp) (p : XProp) :
                    Subtype.val ⁻¹'o r ↪r r

                    The induced relation on a subtype is an embedding under the natural inclusion.

                    Equations
                    Instances For
                      theorem preimage_equivalence {α : Type u_5} {β : Type u_6} (f : αβ) {s : ββProp} (hs : Equivalence s) :
                      def RelEmbedding.toRelHom {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) :
                      r →r s

                      A relation embedding is also a relation homomorphism

                      Equations
                      • f.toRelHom = { toFun := f.toFun, map_rel' := }
                      Instances For
                        instance RelEmbedding.instCoeRelHom {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
                        Coe (r ↪r s) (r →r s)
                        Equations
                        • RelEmbedding.instCoeRelHom = { coe := RelEmbedding.toRelHom }
                        instance RelEmbedding.instFunLike {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
                        FunLike (r ↪r s) α β
                        Equations
                        • RelEmbedding.instFunLike = { coe := fun (x : r ↪r s) => x.toFun, coe_injective' := }
                        instance RelEmbedding.instRelHomClass {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
                        RelHomClass (r ↪r s) r s
                        Equations
                        • =
                        instance RelEmbedding.instEmbeddingLike {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
                        EmbeddingLike (r ↪r s) α β
                        Equations
                        • =
                        @[simp]
                        theorem RelEmbedding.coe_toEmbedding {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {f : r ↪r s} :
                        f.toEmbedding = f
                        @[simp]
                        theorem RelEmbedding.coe_toRelHom {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {f : r ↪r s} :
                        f.toRelHom = f
                        theorem RelEmbedding.toEmbedding_injective {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
                        Function.Injective RelEmbedding.toEmbedding
                        @[simp]
                        theorem RelEmbedding.toEmbedding_inj {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {f : r ↪r s} {g : r ↪r s} :
                        f.toEmbedding = g.toEmbedding f = g
                        theorem RelEmbedding.injective {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) :
                        theorem RelEmbedding.inj {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) {a : α} {b : α} :
                        f a = f b a = b
                        theorem RelEmbedding.map_rel_iff {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) {a : α} {b : α} :
                        s (f a) (f b) r a b
                        @[simp]
                        theorem RelEmbedding.coe_mk {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {f : α β} {h : ∀ {a b : α}, s (f a) (f b) r a b} :
                        { toEmbedding := f, map_rel_iff' := h } = f
                        theorem RelEmbedding.coe_fn_injective {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
                        Function.Injective fun (f : r ↪r s) => f

                        The map coe_fn : (r ↪r s) → (α → β) is injective.

                        theorem RelEmbedding.ext_iff {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {f : r ↪r s} {g : r ↪r s} :
                        f = g ∀ (x : α), f x = g x
                        theorem RelEmbedding.ext {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} ⦃f : r ↪r s ⦃g : r ↪r s (h : ∀ (x : α), f x = g x) :
                        f = g
                        @[simp]
                        theorem RelEmbedding.refl_apply {α : Type u_1} (r : ααProp) (a : α) :
                        def RelEmbedding.refl {α : Type u_1} (r : ααProp) :
                        r ↪r r

                        Identity map is a relation embedding.

                        Equations
                        Instances For
                          def RelEmbedding.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} (f : r ↪r s) (g : s ↪r t) :
                          r ↪r t

                          Composition of two relation embeddings is a relation embedding.

                          Equations
                          • f.trans g = { toEmbedding := f.trans g.toEmbedding, map_rel_iff' := }
                          Instances For
                            instance RelEmbedding.instInhabited {α : Type u_1} (r : ααProp) :
                            Equations
                            theorem RelEmbedding.trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} (f : r ↪r s) (g : s ↪r t) (a : α) :
                            (f.trans g) a = g (f a)
                            @[simp]
                            theorem RelEmbedding.coe_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} (f : r ↪r s) (g : s ↪r t) :
                            (f.trans g) = g f
                            def RelEmbedding.swap {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) :

                            A relation embedding is also a relation embedding between dual relations.

                            Equations
                            • f.swap = { toEmbedding := f.toEmbedding, map_rel_iff' := }
                            Instances For
                              def RelEmbedding.preimage {α : Type u_1} {β : Type u_2} (f : α β) (s : ββProp) :
                              f ⁻¹'o s ↪r s

                              If f is injective, then it is a relation embedding from the preimage relation of s to s.

                              Equations
                              Instances For
                                theorem RelEmbedding.eq_preimage {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) :
                                r = f ⁻¹'o s
                                theorem RelEmbedding.isIrrefl {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) [IsIrrefl β s] :
                                theorem RelEmbedding.isRefl {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) [IsRefl β s] :
                                IsRefl α r
                                theorem RelEmbedding.isSymm {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) [IsSymm β s] :
                                IsSymm α r
                                theorem RelEmbedding.isAsymm {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) [IsAsymm β s] :
                                IsAsymm α r
                                theorem RelEmbedding.isAntisymm {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
                                r ↪r s∀ [inst : IsAntisymm β s], IsAntisymm α r
                                theorem RelEmbedding.isTrans {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
                                r ↪r s∀ [inst : IsTrans β s], IsTrans α r
                                theorem RelEmbedding.isTotal {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
                                r ↪r s∀ [inst : IsTotal β s], IsTotal α r
                                theorem RelEmbedding.isPreorder {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
                                r ↪r s∀ [inst : IsPreorder β s], IsPreorder α r
                                theorem RelEmbedding.isPartialOrder {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
                                r ↪r s∀ [inst : IsPartialOrder β s], IsPartialOrder α r
                                theorem RelEmbedding.isLinearOrder {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
                                r ↪r s∀ [inst : IsLinearOrder β s], IsLinearOrder α r
                                theorem RelEmbedding.isStrictOrder {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
                                r ↪r s∀ [inst : IsStrictOrder β s], IsStrictOrder α r
                                theorem RelEmbedding.isTrichotomous {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
                                r ↪r s∀ [inst : IsTrichotomous β s], IsTrichotomous α r
                                theorem RelEmbedding.isStrictTotalOrder {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
                                r ↪r s∀ [inst : IsStrictTotalOrder β s], IsStrictTotalOrder α r
                                theorem RelEmbedding.acc {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) (a : α) :
                                Acc s (f a)Acc r a
                                theorem RelEmbedding.wellFounded {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
                                r ↪r sWellFounded sWellFounded r
                                theorem RelEmbedding.isWellFounded {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) [IsWellFounded β s] :
                                theorem RelEmbedding.isWellOrder {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
                                r ↪r s∀ [inst : IsWellOrder β s], IsWellOrder α r
                                instance Subtype.wellFoundedLT {α : Type u_1} [LT α] [WellFoundedLT α] (p : αProp) :
                                Equations
                                • =
                                instance Subtype.wellFoundedGT {α : Type u_1} [LT α] [WellFoundedGT α] (p : αProp) :
                                Equations
                                • =
                                @[simp]
                                theorem Quotient.mkRelHom_apply {α : Type u_1} :
                                ∀ {x : Setoid α} {r : ααProp} (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ a₂b₁ b₂r a₁ b₁ = r a₂ b₂) (a : α), (Quotient.mkRelHom H) a = a
                                def Quotient.mkRelHom {α : Type u_1} :
                                {x : Setoid α} → {r : ααProp} → (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ a₂b₁ b₂r a₁ b₁ = r a₂ b₂) → r →r Quotient.lift₂ r H

                                Quotient.mk as a relation homomorphism between the relation and the lift of a relation.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem Quotient.outRelEmbedding_apply {α : Type u_1} :
                                  ∀ {x : Setoid α} {r : ααProp} (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ a₂b₁ b₂r a₁ b₁ = r a₂ b₂) (a : Quotient x), (Quotient.outRelEmbedding H) a = a.out
                                  noncomputable def Quotient.outRelEmbedding {α : Type u_1} :
                                  {x : Setoid α} → {r : ααProp} → (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ a₂b₁ b₂r a₁ b₁ = r a₂ b₂) → Quotient.lift₂ r H ↪r r

                                  Quotient.out as a relation embedding between the lift of a relation and the relation.

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem Quotient.out'RelEmbedding_apply {α : Type u_1} :
                                    ∀ {x : Setoid α} {r : ααProp} (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ a₂b₁ b₂r a₁ b₁ = r a₂ b₂) (a : Quotient x), (Quotient.out'RelEmbedding H) a = a.out'
                                    noncomputable def Quotient.out'RelEmbedding {α : Type u_1} :
                                    {x : Setoid α} → {r : ααProp} → (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ a₂b₁ b₂r a₁ b₁ = r a₂ b₂) → (fun (a b : Quotient x) => a.liftOn₂' b r H) ↪r r

                                    Quotient.out' as a relation embedding between the lift of a relation and the relation.

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem acc_lift₂_iff {α : Type u_1} :
                                      ∀ {x : Setoid α} {r : ααProp} {H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ a₂b₁ b₂r a₁ b₁ = r a₂ b₂} {a : α}, Acc (Quotient.lift₂ r H) a Acc r a
                                      @[simp]
                                      theorem acc_liftOn₂'_iff {α : Type u_1} {s : Setoid α} {r : ααProp} {H : ∀ (a₁ a₂ b₁ b₂ : α), s a₁ b₁s a₂ b₂r a₁ a₂ = r b₁ b₂} {a : α} :
                                      Acc (fun (x y : Quotient s) => x.liftOn₂' y r H) (Quotient.mk'' a) Acc r a
                                      @[simp]
                                      theorem wellFounded_lift₂_iff {α : Type u_1} :
                                      ∀ {x : Setoid α} {r : ααProp} {H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ a₂b₁ b₂r a₁ b₁ = r a₂ b₂}, WellFounded (Quotient.lift₂ r H) WellFounded r

                                      A relation is well founded iff its lift to a quotient is.

                                      theorem WellFounded.of_quotient_lift₂ {α : Type u_1} :
                                      ∀ {x : Setoid α} {r : ααProp} {H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ a₂b₁ b₂r a₁ b₁ = r a₂ b₂}, WellFounded (Quotient.lift₂ r H)WellFounded r

                                      Alias of the forward direction of wellFounded_lift₂_iff.


                                      A relation is well founded iff its lift to a quotient is.

                                      theorem WellFounded.quotient_lift₂ {α : Type u_1} :
                                      ∀ {x : Setoid α} {r : ααProp} {H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ a₂b₁ b₂r a₁ b₁ = r a₂ b₂}, WellFounded rWellFounded (Quotient.lift₂ r H)

                                      Alias of the reverse direction of wellFounded_lift₂_iff.


                                      A relation is well founded iff its lift to a quotient is.

                                      @[simp]
                                      theorem wellFounded_liftOn₂'_iff {α : Type u_1} {s : Setoid α} {r : ααProp} {H : ∀ (a₁ a₂ b₁ b₂ : α), s a₁ b₁s a₂ b₂r a₁ a₂ = r b₁ b₂} :
                                      (WellFounded fun (x y : Quotient s) => x.liftOn₂' y r H) WellFounded r
                                      theorem WellFounded.of_quotient_liftOn₂' {α : Type u_1} {s : Setoid α} {r : ααProp} {H : ∀ (a₁ a₂ b₁ b₂ : α), s a₁ b₁s a₂ b₂r a₁ a₂ = r b₁ b₂} :
                                      (WellFounded fun (x y : Quotient s) => x.liftOn₂' y r H)WellFounded r

                                      Alias of the forward direction of wellFounded_liftOn₂'_iff.

                                      theorem WellFounded.quotient_liftOn₂' {α : Type u_1} {s : Setoid α} {r : ααProp} {H : ∀ (a₁ a₂ b₁ b₂ : α), s a₁ b₁s a₂ b₂r a₁ a₂ = r b₁ b₂} :
                                      WellFounded rWellFounded fun (x y : Quotient s) => x.liftOn₂' y r H

                                      Alias of the reverse direction of wellFounded_liftOn₂'_iff.

                                      def RelEmbedding.ofMapRelIff {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : αβ) [IsAntisymm α r] [IsRefl β s] (hf : ∀ (a b : α), s (f a) (f b) r a b) :
                                      r ↪r s

                                      To define a relation embedding from an antisymmetric relation r to a reflexive relation s it suffices to give a function together with a proof that it satisfies s (f a) (f b) ↔ r a b.

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem RelEmbedding.ofMapRelIff_coe {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : αβ) [IsAntisymm α r] [IsRefl β s] (hf : ∀ (a b : α), s (f a) (f b) r a b) :
                                        def RelEmbedding.ofMonotone {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsTrichotomous α r] [IsAsymm β s] (f : αβ) (H : ∀ (a b : α), r a bs (f a) (f b)) :
                                        r ↪r s

                                        It suffices to prove f is monotone between strict relations to show it is a relation embedding.

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem RelEmbedding.ofMonotone_coe {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsTrichotomous α r] [IsAsymm β s] (f : αβ) (H : ∀ (a b : α), r a bs (f a) (f b)) :
                                          def RelEmbedding.ofIsEmpty {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsEmpty α] :
                                          r ↪r s

                                          A relation embedding from an empty type.

                                          Equations
                                          Instances For
                                            @[simp]
                                            theorem RelEmbedding.sumLiftRelInl_apply {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) (val : α) :
                                            def RelEmbedding.sumLiftRelInl {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) :

                                            Sum.inl as a relation embedding into Sum.LiftRel r s.

                                            Equations
                                            Instances For
                                              @[simp]
                                              theorem RelEmbedding.sumLiftRelInr_apply {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) (val : β) :
                                              def RelEmbedding.sumLiftRelInr {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) :

                                              Sum.inr as a relation embedding into Sum.LiftRel r s.

                                              Equations
                                              Instances For
                                                @[simp]
                                                theorem RelEmbedding.sumLiftRelMap_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : ααProp} {s : ββProp} {t : γγProp} {u : δδProp} (f : r ↪r s) (g : t ↪r u) :
                                                ∀ (a : α γ), (f.sumLiftRelMap g) a = Sum.map (⇑f) (⇑g) a
                                                def RelEmbedding.sumLiftRelMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : ααProp} {s : ββProp} {t : γγProp} {u : δδProp} (f : r ↪r s) (g : t ↪r u) :

                                                Sum.map as a relation embedding between Sum.LiftRel relations.

                                                Equations
                                                • f.sumLiftRelMap g = { toFun := Sum.map f g, inj' := , map_rel_iff' := }
                                                Instances For
                                                  @[simp]
                                                  theorem RelEmbedding.sumLexInl_apply {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) (val : α) :
                                                  def RelEmbedding.sumLexInl {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) :

                                                  Sum.inl as a relation embedding into Sum.Lex r s.

                                                  Equations
                                                  Instances For
                                                    @[simp]
                                                    theorem RelEmbedding.sumLexInr_apply {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) (val : β) :
                                                    def RelEmbedding.sumLexInr {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) :

                                                    Sum.inr as a relation embedding into Sum.Lex r s.

                                                    Equations
                                                    Instances For
                                                      @[simp]
                                                      theorem RelEmbedding.sumLexMap_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : ααProp} {s : ββProp} {t : γγProp} {u : δδProp} (f : r ↪r s) (g : t ↪r u) :
                                                      ∀ (a : α γ), (f.sumLexMap g) a = Sum.map (⇑f) (⇑g) a
                                                      def RelEmbedding.sumLexMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : ααProp} {s : ββProp} {t : γγProp} {u : δδProp} (f : r ↪r s) (g : t ↪r u) :

                                                      Sum.map as a relation embedding between Sum.Lex relations.

                                                      Equations
                                                      • f.sumLexMap g = { toFun := Sum.map f g, inj' := , map_rel_iff' := }
                                                      Instances For
                                                        @[simp]
                                                        theorem RelEmbedding.prodLexMkLeft_apply {α : Type u_1} {β : Type u_2} {r : ααProp} (s : ββProp) {a : α} (h : ¬r a a) (snd : β) :
                                                        (RelEmbedding.prodLexMkLeft s h) snd = (a, snd)
                                                        def RelEmbedding.prodLexMkLeft {α : Type u_1} {β : Type u_2} {r : ααProp} (s : ββProp) {a : α} (h : ¬r a a) :

                                                        fun b ↦ Prod.mk a b as a relation embedding.

                                                        Equations
                                                        Instances For
                                                          @[simp]
                                                          theorem RelEmbedding.prodLexMkRight_apply {α : Type u_1} {β : Type u_2} {s : ββProp} (r : ααProp) {b : β} (h : ¬s b b) (a : α) :
                                                          def RelEmbedding.prodLexMkRight {α : Type u_1} {β : Type u_2} {s : ββProp} (r : ααProp) {b : β} (h : ¬s b b) :

                                                          fun a ↦ Prod.mk a b as a relation embedding.

                                                          Equations
                                                          Instances For
                                                            @[simp]
                                                            theorem RelEmbedding.prodLexMap_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : ααProp} {s : ββProp} {t : γγProp} {u : δδProp} (f : r ↪r s) (g : t ↪r u) :
                                                            ∀ (a : α × γ), (f.prodLexMap g) a = Prod.map (⇑f) (⇑g) a
                                                            def RelEmbedding.prodLexMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : ααProp} {s : ββProp} {t : γγProp} {u : δδProp} (f : r ↪r s) (g : t ↪r u) :

                                                            Prod.map as a relation embedding.

                                                            Equations
                                                            • f.prodLexMap g = { toFun := Prod.map f g, inj' := , map_rel_iff' := }
                                                            Instances For
                                                              structure RelIso {α : Type u_5} {β : Type u_6} (r : ααProp) (s : ββProp) extends Equiv :
                                                              Type (max u_5 u_6)

                                                              A relation isomorphism is an equivalence that is also a relation embedding.

                                                              • toFun : αβ
                                                              • invFun : βα
                                                              • left_inv : Function.LeftInverse self.invFun self.toFun
                                                              • right_inv : Function.RightInverse self.invFun self.toFun
                                                              • map_rel_iff' : ∀ {a b : α}, s (self.toEquiv a) (self.toEquiv b) r a b

                                                                Elements are related iff they are related after apply a RelIso

                                                              Instances For
                                                                theorem RelIso.map_rel_iff' {α : Type u_5} {β : Type u_6} {r : ααProp} {s : ββProp} (self : r ≃r s) {a : α} {b : α} :
                                                                s (self.toEquiv a) (self.toEquiv b) r a b

                                                                Elements are related iff they are related after apply a RelIso

                                                                A relation isomorphism is an equivalence that is also a relation embedding.

                                                                Equations
                                                                Instances For
                                                                  def RelIso.toRelEmbedding {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≃r s) :
                                                                  r ↪r s

                                                                  Convert a RelIso to a RelEmbedding. This function is also available as a coercion but often it is easier to write f.toRelEmbedding than to write explicitly r and s in the target type.

                                                                  Equations
                                                                  • f.toRelEmbedding = { toEmbedding := f.toEmbedding, map_rel_iff' := }
                                                                  Instances For
                                                                    theorem RelIso.toEquiv_injective {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
                                                                    Function.Injective RelIso.toEquiv
                                                                    instance RelIso.instCoeOutRelEmbedding {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
                                                                    CoeOut (r ≃r s) (r ↪r s)
                                                                    Equations
                                                                    • RelIso.instCoeOutRelEmbedding = { coe := RelIso.toRelEmbedding }
                                                                    instance RelIso.instFunLike {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
                                                                    FunLike (r ≃r s) α β
                                                                    Equations
                                                                    • RelIso.instFunLike = { coe := fun (x : r ≃r s) => x.toRelEmbedding, coe_injective' := }
                                                                    instance RelIso.instRelHomClass {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
                                                                    RelHomClass (r ≃r s) r s
                                                                    Equations
                                                                    • =
                                                                    instance RelIso.instEquivLike {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
                                                                    EquivLike (r ≃r s) α β
                                                                    Equations
                                                                    • RelIso.instEquivLike = { coe := fun (f : r ≃r s) => f, inv := fun (f : r ≃r s) => f.symm, left_inv := , right_inv := , coe_injective' := }
                                                                    @[simp]
                                                                    theorem RelIso.coe_toRelEmbedding {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≃r s) :
                                                                    f.toRelEmbedding = f
                                                                    @[simp]
                                                                    theorem RelIso.coe_toEmbedding {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≃r s) :
                                                                    f.toEmbedding = f
                                                                    theorem RelIso.map_rel_iff {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≃r s) {a : α} {b : α} :
                                                                    s (f a) (f b) r a b
                                                                    @[simp]
                                                                    theorem RelIso.coe_fn_mk {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : α β) (o : ∀ ⦃a b : α⦄, s (f a) (f b) r a b) :
                                                                    { toEquiv := f, map_rel_iff' := o } = f
                                                                    @[simp]
                                                                    theorem RelIso.coe_fn_toEquiv {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≃r s) :
                                                                    f.toEquiv = f
                                                                    theorem RelIso.coe_fn_injective {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
                                                                    Function.Injective fun (f : r ≃r s) => f

                                                                    The map DFunLike.coe : (r ≃r s) → (α → β) is injective.

                                                                    theorem RelIso.ext_iff {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {f : r ≃r s} {g : r ≃r s} :
                                                                    f = g ∀ (x : α), f x = g x
                                                                    theorem RelIso.ext {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} ⦃f : r ≃r s ⦃g : r ≃r s (h : ∀ (x : α), f x = g x) :
                                                                    f = g
                                                                    def RelIso.symm {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≃r s) :
                                                                    s ≃r r

                                                                    Inverse map of a relation isomorphism is a relation isomorphism.

                                                                    Equations
                                                                    • f.symm = { toEquiv := f.symm, map_rel_iff' := }
                                                                    Instances For
                                                                      def RelIso.Simps.apply {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (h : r ≃r s) :
                                                                      αβ

                                                                      See Note [custom simps projection]. We need to specify this projection explicitly in this case, because RelIso defines custom coercions other than the ones given by DFunLike.

                                                                      Equations
                                                                      Instances For
                                                                        def RelIso.Simps.symm_apply {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (h : r ≃r s) :
                                                                        βα

                                                                        See Note [custom simps projection].

                                                                        Equations
                                                                        Instances For
                                                                          @[simp]
                                                                          theorem RelIso.refl_apply {α : Type u_1} (r : ααProp) (a : α) :
                                                                          (RelIso.refl r) a = a
                                                                          def RelIso.refl {α : Type u_1} (r : ααProp) :
                                                                          r ≃r r

                                                                          Identity map is a relation isomorphism.

                                                                          Equations
                                                                          Instances For
                                                                            @[simp]
                                                                            theorem RelIso.trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} (f₁ : r ≃r s) (f₂ : s ≃r t) :
                                                                            ∀ (a : α), (f₁.trans f₂) a = f₂ (f₁ a)
                                                                            def RelIso.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} (f₁ : r ≃r s) (f₂ : s ≃r t) :
                                                                            r ≃r t

                                                                            Composition of two relation isomorphisms is a relation isomorphism.

                                                                            Equations
                                                                            • f₁.trans f₂ = { toEquiv := f₁.trans f₂.toEquiv, map_rel_iff' := }
                                                                            Instances For
                                                                              instance RelIso.instInhabited {α : Type u_1} (r : ααProp) :
                                                                              Equations
                                                                              @[simp]
                                                                              theorem RelIso.default_def {α : Type u_1} (r : ααProp) :
                                                                              default = RelIso.refl r
                                                                              @[simp]
                                                                              theorem RelIso.cast_toEquiv {α : Type u} {β : Type u} {r : ααProp} {s : ββProp} (h₁ : α = β) (h₂ : HEq r s) :
                                                                              (RelIso.cast h₁ h₂).toEquiv = Equiv.cast h₁
                                                                              @[simp]
                                                                              theorem RelIso.cast_apply {α : Type u} {β : Type u} {r : ααProp} {s : ββProp} (h₁ : α = β) (h₂ : HEq r s) (a : α) :
                                                                              (RelIso.cast h₁ h₂) a = cast h₁ a
                                                                              def RelIso.cast {α : Type u} {β : Type u} {r : ααProp} {s : ββProp} (h₁ : α = β) (h₂ : HEq r s) :
                                                                              r ≃r s

                                                                              A relation isomorphism between equal relations on equal types.

                                                                              Equations
                                                                              Instances For
                                                                                @[simp]
                                                                                theorem RelIso.cast_symm {α : Type u} {β : Type u} {r : ααProp} {s : ββProp} (h₁ : α = β) (h₂ : HEq r s) :
                                                                                (RelIso.cast h₁ h₂).symm = RelIso.cast
                                                                                @[simp]
                                                                                theorem RelIso.cast_refl {α : Type u} {r : ααProp} (h₁ : optParam (α = α) ) (h₂ : optParam (HEq r r) ) :
                                                                                @[simp]
                                                                                theorem RelIso.cast_trans {α : Type u} {β : Type u} {γ : Type u} {r : ααProp} {s : ββProp} {t : γγProp} (h₁ : α = β) (h₁' : β = γ) (h₂ : HEq r s) (h₂' : HEq s t) :
                                                                                (RelIso.cast h₁ h₂).trans (RelIso.cast h₁' h₂') = RelIso.cast
                                                                                def RelIso.swap {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≃r s) :

                                                                                a relation isomorphism is also a relation isomorphism between dual relations.

                                                                                Equations
                                                                                • f.swap = { toEquiv := f.toEquiv, map_rel_iff' := }
                                                                                Instances For
                                                                                  @[simp]
                                                                                  theorem RelIso.coe_fn_symm_mk {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : α β) (o : ∀ {a b : α}, s (f a) (f b) r a b) :
                                                                                  { toEquiv := f, map_rel_iff' := o }.symm = f.symm
                                                                                  @[simp]
                                                                                  theorem RelIso.apply_symm_apply {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (e : r ≃r s) (x : β) :
                                                                                  e (e.symm x) = x
                                                                                  @[simp]
                                                                                  theorem RelIso.symm_apply_apply {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (e : r ≃r s) (x : α) :
                                                                                  e.symm (e x) = x
                                                                                  theorem RelIso.rel_symm_apply {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (e : r ≃r s) {x : α} {y : β} :
                                                                                  r x (e.symm y) s (e x) y
                                                                                  theorem RelIso.symm_apply_rel {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (e : r ≃r s) {x : β} {y : α} :
                                                                                  r (e.symm x) y s x (e y)
                                                                                  @[simp]
                                                                                  theorem RelIso.self_trans_symm {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (e : r ≃r s) :
                                                                                  e.trans e.symm = RelIso.refl r
                                                                                  @[simp]
                                                                                  theorem RelIso.symm_trans_self {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (e : r ≃r s) :
                                                                                  e.symm.trans e = RelIso.refl s
                                                                                  theorem RelIso.bijective {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (e : r ≃r s) :
                                                                                  theorem RelIso.injective {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (e : r ≃r s) :
                                                                                  theorem RelIso.surjective {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (e : r ≃r s) :
                                                                                  theorem RelIso.eq_iff_eq {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≃r s) {a : α} {b : α} :
                                                                                  f a = f b a = b
                                                                                  def RelIso.preimage {α : Type u_1} {β : Type u_2} (f : α β) (s : ββProp) :
                                                                                  f ⁻¹'o s ≃r s

                                                                                  Any equivalence lifts to a relation isomorphism between s and its preimage.

                                                                                  Equations
                                                                                  Instances For
                                                                                    instance RelIso.IsWellOrder.preimage {β : Type u_2} {α : Type u} (r : ααProp) [IsWellOrder α r] (f : β α) :
                                                                                    IsWellOrder β (f ⁻¹'o r)
                                                                                    Equations
                                                                                    • =
                                                                                    instance RelIso.IsWellOrder.ulift {α : Type u} (r : ααProp) [IsWellOrder α r] :
                                                                                    IsWellOrder (ULift.{u_5, u} α) (ULift.down ⁻¹'o r)
                                                                                    Equations
                                                                                    • =
                                                                                    @[simp]
                                                                                    theorem RelIso.ofSurjective_apply {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) (H : Function.Surjective f) (a : α) :
                                                                                    noncomputable def RelIso.ofSurjective {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) (H : Function.Surjective f) :
                                                                                    r ≃r s

                                                                                    A surjective relation embedding is a relation isomorphism.

                                                                                    Equations
                                                                                    Instances For
                                                                                      def RelIso.sumLexCongr {α₁ : Type u_5} {α₂ : Type u_6} {β₁ : Type u_7} {β₂ : Type u_8} {r₁ : α₁α₁Prop} {r₂ : α₂α₂Prop} {s₁ : β₁β₁Prop} {s₂ : β₂β₂Prop} (e₁ : r₁ ≃r s₁) (e₂ : r₂ ≃r s₂) :
                                                                                      Sum.Lex r₁ r₂ ≃r Sum.Lex s₁ s₂

                                                                                      Given relation isomorphisms r₁ ≃r s₁ and r₂ ≃r s₂, construct a relation isomorphism for the lexicographic orders on the sum.

                                                                                      Equations
                                                                                      • e₁.sumLexCongr e₂ = { toEquiv := e₁.sumCongr e₂.toEquiv, map_rel_iff' := }
                                                                                      Instances For
                                                                                        def RelIso.prodLexCongr {α₁ : Type u_5} {α₂ : Type u_6} {β₁ : Type u_7} {β₂ : Type u_8} {r₁ : α₁α₁Prop} {r₂ : α₂α₂Prop} {s₁ : β₁β₁Prop} {s₂ : β₂β₂Prop} (e₁ : r₁ ≃r s₁) (e₂ : r₂ ≃r s₂) :
                                                                                        Prod.Lex r₁ r₂ ≃r Prod.Lex s₁ s₂

                                                                                        Given relation isomorphisms r₁ ≃r s₁ and r₂ ≃r s₂, construct a relation isomorphism for the lexicographic orders on the product.

                                                                                        Equations
                                                                                        • e₁.prodLexCongr e₂ = { toEquiv := e₁.prodCongr e₂.toEquiv, map_rel_iff' := }
                                                                                        Instances For
                                                                                          def RelIso.relIsoOfIsEmpty {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsEmpty α] [IsEmpty β] :
                                                                                          r ≃r s

                                                                                          Two relations on empty types are isomorphic.

                                                                                          Equations
                                                                                          Instances For
                                                                                            def RelIso.relIsoOfUniqueOfIrrefl {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsIrrefl α r] [IsIrrefl β s] [Unique α] [Unique β] :
                                                                                            r ≃r s

                                                                                            Two irreflexive relations on a unique type are isomorphic.

                                                                                            Equations
                                                                                            Instances For
                                                                                              def RelIso.relIsoOfUniqueOfRefl {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsRefl α r] [IsRefl β s] [Unique α] [Unique β] :
                                                                                              r ≃r s

                                                                                              Two reflexive relations on a unique type are isomorphic.

                                                                                              Equations
                                                                                              Instances For