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_1} {β : Type u_2} (r : ααProp) (s : ββProp) :
Type (maxu_1u_2)
  • The underlying function of a RelHom

    toFun : αβ
  • A RelHom sends related elements to related elements

    map_rel' : {a b : α} → r a bs (toFun a) (toFun b)

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)→ s (f a) (f b).

Instances For

    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)→ s (f a) (f b).

    Equations
    class RelHomClass (F : Type u_1) {α : outParam (Type u_2)} {β : outParam (Type u_3)} (r : outParam (ααProp)) (s : outParam (ββProp)) extends FunLike :
    Type (max(maxu_1u_2)u_3)
    • A RelHomClass sends related elements to related elements

      map_rel : (f : F) → {a b : α} → r a bs (f a) (f b)

    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)→ 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.

    Instances
      theorem RelHomClass.isIrrefl {α : Type u_2} {β : Type u_3} {r : ααProp} {s : ββProp} {F : Type u_1} [inst : RelHomClass F r s] (f : F) [inst : IsIrrefl β s] :
      theorem RelHomClass.isAsymm {α : Type u_2} {β : Type u_3} {r : ααProp} {s : ββProp} {F : Type u_1} [inst : RelHomClass F r s] (f : F) [inst : IsAsymm β s] :
      IsAsymm α r
      theorem RelHomClass.acc {α : Type u_2} {β : Type u_3} {r : ααProp} {s : ββProp} {F : Type u_1} [inst : RelHomClass F r s] (f : F) (a : α) :
      Acc s (f a)Acc r a
      theorem RelHomClass.wellFounded {α : Type u_2} {β : Type u_3} {r : ααProp} {s : ββProp} {F : Type u_1} [inst : RelHomClass F r s] (f : F) :
      instance RelHom.instRelHomClassRelHom {α : 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 => f

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

      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
      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
      @[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
      @[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 : α) :
      ↑(RelHom.comp g 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
      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
      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
      theorem injective_of_increasing {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [inst : IsTrichotomous α r] [inst : 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} [inst : IsTrichotomous α r] [inst : IsIrrefl β s] (f : r →r s) :

      An increasing function is injective

      theorem 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_1} {β : Type u_2} (r : ααProp) (s : ββProp) extends Function.Embedding :
      Type (maxu_1u_2)
      • Elements are related iff they are related after apply a RelEmbedding

        map_rel_iff' : ∀ {a b : α}, s (toEmbedding a) (toEmbedding b) r a b

      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)↔ s (f a) (f b).

      Instances For

        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)↔ s (f a) (f b).

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

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

        Equations
        • One or more equations did not get rendered due to their size.
        theorem preimage_equivalence {α : Sort u_1} {β : Sort u_2} (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
        instance RelEmbedding.instCoeRelEmbeddingRelHom {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
        Coe (r ↪r s) (r →r s)
        Equations
        • RelEmbedding.instCoeRelEmbeddingRelHom = { coe := RelEmbedding.toRelHom }
        instance RelEmbedding.instCoeFunRelEmbeddingForAll {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
        CoeFun (r ↪r s) fun x => αβ
        Equations
        • RelEmbedding.instCoeFunRelEmbeddingForAll = { coe := fun o => o.toEmbedding }
        instance RelEmbedding.instRelHomClassRelEmbedding {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
        RelHomClass (r ↪r s) r s
        Equations
        • RelEmbedding.instRelHomClassRelEmbedding = RelHomClass.mk RelEmbedding.instRelHomClassRelEmbedding.proof_2
        def RelEmbedding.Simps.apply {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (h : r ↪r s) :
        αβ

        See Note [custom simps projection]. We specify this explicitly because we have a coercion not given by the FunLike instance. Todo: remove that instance?

        Equations
        theorem RelEmbedding.injective {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) :
        Function.Injective f.toEmbedding
        theorem RelEmbedding.inj {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) {a : α} {b : α} :
        f.toEmbedding a = f.toEmbedding 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.toEmbedding a) (f.toEmbedding b) r a b
        theorem RelEmbedding.coe_fn_injective {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
        Function.Injective fun f => f.toEmbedding

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

        theorem RelEmbedding.ext {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} ⦃f : r ↪r s ⦃g : r ↪r s (h : ∀ (x : α), f.toEmbedding x = g.toEmbedding x) :
        f = g
        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.toEmbedding x = g.toEmbedding x
        @[simp]
        theorem RelEmbedding.refl_apply {α : Type u_1} (r : ααProp) (a : α) :
        (RelEmbedding.refl r).toEmbedding a = a
        def RelEmbedding.refl {α : Type u_1} (r : ααProp) :
        r ↪r r

        Identity map is a relation embedding.

        Equations
        • One or more equations did not get rendered due to their size.
        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
        • One or more equations did not get rendered due to their size.
        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 : α) :
        (RelEmbedding.trans f g).toEmbedding a = g.toEmbedding (f.toEmbedding 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) :
        (RelEmbedding.trans f g).toEmbedding = g.toEmbedding f.toEmbedding
        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
        • RelEmbedding.swap f = { toEmbedding := f.toEmbedding, map_rel_iff' := (_ : ∀ {a b : α}, s (f.toEmbedding b) (f.toEmbedding a) r b a) }
        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
        • RelEmbedding.preimage f s = { toEmbedding := f, map_rel_iff' := (_ : ∀ {a b : α}, s (f a) (f b) s (f a) (f b)) }
        theorem RelEmbedding.eq_preimage {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) :
        r = f.toEmbedding ⁻¹'o s
        theorem RelEmbedding.isIrrefl {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) [inst : IsIrrefl β s] :
        theorem RelEmbedding.isRefl {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) [inst : IsRefl β s] :
        IsRefl α r
        theorem RelEmbedding.isSymm {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) [inst : IsSymm β s] :
        IsSymm α r
        theorem RelEmbedding.isAsymm {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) [inst : 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.toEmbedding a)Acc r a
        theorem RelEmbedding.wellFounded {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
        r ↪r sWellFounded sWellFounded r
        theorem RelEmbedding.isWellOrder {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
        r ↪r s∀ [inst : IsWellOrder β s], IsWellOrder α r
        @[simp]
        theorem Quotient.outRelEmbedding_apply {α : Type u_1} [s : Setoid α] {r : ααProp} (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ a₂b₁ b₂r a₁ b₁ = r a₂ b₂) :
        ∀ (a : Quotient s), (Quotient.outRelEmbedding H).toEmbedding a = Quotient.out a
        noncomputable def Quotient.outRelEmbedding {α : Type u_1} [s : Setoid α] {r : ααProp} (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ a₂b₁ b₂r a₁ b₁ = r a₂ b₂) :

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

        Equations
        • One or more equations did not get rendered due to their size.
        @[simp]
        theorem wellFounded_lift₂_iff {α : Type u_1} [s : Setoid α] {r : ααProp} {H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ a₂b₁ b₂r a₁ b₁ = r a₂ b₂} :

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

        theorem RelEmbedding.WellFounded.quotient_lift₂ {α : Type u_1} [s : Setoid α] {r : ααProp} {H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ a₂b₁ b₂r a₁ b₁ = r a₂ b₂} :

        Alias of the reverse direction of wellFounded_lift₂_iff.

        theorem RelEmbedding.WellFounded.of_quotient_lift₂ {α : Type u_1} [s : Setoid α] {r : ααProp} {H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ a₂b₁ b₂r a₁ b₁ = r a₂ b₂} :

        Alias of the forward direction of wellFounded_lift₂_iff.

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

        To define an 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↔ r a b.

        Equations
        • RelEmbedding.ofMapRelIff f hf = { toEmbedding := { toFun := f, inj' := (_ : ∀ (x x_1 : α), f x = f x_1x = x_1) }, map_rel_iff' := (_ : ∀ {a b : α}, s (f a) (f b) r a b) }
        @[simp]
        theorem RelEmbedding.ofMapRelIff_coe {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : αβ) [inst : IsAntisymm α r] [inst : IsRefl β s] (hf : ∀ (a b : α), s (f a) (f b) r a b) :
        (RelEmbedding.ofMapRelIff f hf).toEmbedding = f
        def RelEmbedding.ofMonotone {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [inst : IsTrichotomous α r] [inst : 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
        • One or more equations did not get rendered due to their size.
        @[simp]
        theorem RelEmbedding.ofMonotone_coe {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [inst : IsTrichotomous α r] [inst : IsAsymm β s] (f : αβ) (H : (a b : α) → r a bs (f a) (f b)) :
        (RelEmbedding.ofMonotone f H).toEmbedding = f
        def RelEmbedding.ofIsEmpty {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [inst : IsEmpty α] :
        r ↪r s

        A relation embedding from an empty type.

        Equations
        • One or more equations did not get rendered due to their size.
        @[simp]
        theorem RelEmbedding.sumLiftRelInl_apply {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) (val : α) :
        (RelEmbedding.sumLiftRelInl r s).toEmbedding val = Sum.inl 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
        • One or more equations did not get rendered due to their size.
        @[simp]
        theorem RelEmbedding.sumLiftRelInr_apply {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) (val : β) :
        (RelEmbedding.sumLiftRelInr r s).toEmbedding val = Sum.inr 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
        • One or more equations did not get rendered due to their size.
        @[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 : α γ), (RelEmbedding.sumLiftRelMap f g).toEmbedding a = Sum.map (f.toEmbedding) (g.toEmbedding) 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
        • One or more equations did not get rendered due to their size.
        @[simp]
        theorem RelEmbedding.sumLexInl_apply {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) (val : α) :
        (RelEmbedding.sumLexInl r s).toEmbedding val = Sum.inl 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
        @[simp]
        theorem RelEmbedding.sumLexInr_apply {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) (val : β) :
        (RelEmbedding.sumLexInr r s).toEmbedding val = Sum.inr 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
        @[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 : α γ), (RelEmbedding.sumLexMap f g).toEmbedding a = Sum.map (f.toEmbedding) (g.toEmbedding) 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
        • One or more equations did not get rendered due to their size.
        @[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).toEmbedding snd = (a, snd)
        def RelEmbedding.prodLexMkLeft {α : Type u_1} {β : Type u_2} {r : ααProp} (s : ββProp) {a : α} (h : ¬r a a) :

        λ b, Prod.mk a b as a relation embedding.

        Equations
        • One or more equations did not get rendered due to their size.
        @[simp]
        theorem RelEmbedding.prodLexMkRight_apply {α : Type u_1} {β : Type u_2} {s : ββProp} (r : ααProp) {b : β} (h : ¬s b b) (a : α) :
        (RelEmbedding.prodLexMkRight r h).toEmbedding a = (a, b)
        def RelEmbedding.prodLexMkRight {α : Type u_1} {β : Type u_2} {s : ββProp} (r : ααProp) {b : β} (h : ¬s b b) :

        λ a, Prod.mk a b as a relation embedding.

        Equations
        • One or more equations did not get rendered due to their size.
        @[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 : α × γ), (RelEmbedding.prodLexMap f g).toEmbedding a = Prod.map (f.toEmbedding) (g.toEmbedding) 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
        • One or more equations did not get rendered due to their size.
        structure RelIso {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) extends Equiv :
        Type (maxu_1u_2)
        • Elements are related iff they are related after apply a RelIso

          map_rel_iff' : ∀ {a b : α}, s (toEquiv a) (toEquiv b) r a b

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

        Instances For

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

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

          Convert an 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
          theorem RelIso.toEquiv_injective {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
          Function.Injective RelIso.toEquiv
          instance RelIso.instCoeOutRelIsoRelEmbedding {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
          CoeOut (r ≃r s) (r ↪r s)
          Equations
          • RelIso.instCoeOutRelIsoRelEmbedding = { coe := RelIso.toRelEmbedding }
          instance RelIso.instCoeFunRelIsoForAll {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
          CoeFun (r ≃r s) fun x => αβ
          Equations
          instance RelIso.instRelHomClassRelIso {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
          RelHomClass (r ≃r s) r s
          Equations
          • RelIso.instRelHomClassRelIso = RelHomClass.mk RelIso.instRelHomClassRelIso.proof_2
          theorem RelIso.map_rel_iff {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≃r s) {a : α} {b : α} :
          s ((RelIso.toRelEmbedding f).toEmbedding a) ((RelIso.toRelEmbedding f).toEmbedding 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) :
          (RelIso.toRelEmbedding { toEquiv := f, map_rel_iff' := o }).toEmbedding = f
          @[simp]
          theorem RelIso.coe_fn_toEquiv {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≃r s) :
          f.toEquiv = (RelIso.toRelEmbedding f).toEmbedding
          theorem RelIso.coe_fn_injective {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
          Function.Injective fun f => (RelIso.toRelEmbedding f).toEmbedding

          The map coe_fn : (r ≃r s) → (α → β)≃r s) → (α → β)→ (α → β)→ β) is injective. Lean fails to parse function.injective (λ e : r ≃r s, (e : α → β))≃r s, (e : α → β))→ β)), so we use a trick to say the same.

          theorem RelIso.ext {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} ⦃f : r ≃r s ⦃g : r ≃r s (h : ∀ (x : α), (RelIso.toRelEmbedding f).toEmbedding x = (RelIso.toRelEmbedding g).toEmbedding x) :
          f = g
          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 : α), (RelIso.toRelEmbedding f).toEmbedding x = (RelIso.toRelEmbedding g).toEmbedding x
          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
          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 FunLike.

          Equations
          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
          @[simp]
          theorem RelIso.refl_apply {α : Type u_1} (r : ααProp) (a : α) :
          (RelIso.toRelEmbedding (RelIso.refl r)).toEmbedding a = a
          def RelIso.refl {α : Type u_1} (r : ααProp) :
          r ≃r r

          Identity map is a relation isomorphism.

          Equations
          @[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 : α), (RelIso.toRelEmbedding (RelIso.trans f₁ f₂)).toEmbedding a = (RelIso.toRelEmbedding f₂).toEmbedding ((RelIso.toRelEmbedding f₁).toEmbedding 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
          • One or more equations did not get rendered due to their size.
          instance RelIso.instInhabitedRelIso {α : 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.toRelEmbedding (RelIso.cast h₁ h₂)).toEmbedding 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
          @[simp]
          theorem RelIso.cast_symm {α : Type u} {β : Type u} {r : ααProp} {s : ββProp} (h₁ : α = β) (h₂ : HEq r s) :
          RelIso.symm (RelIso.cast h₁ h₂) = RelIso.cast (_ : β = α) (_ : HEq s r)
          @[simp]
          theorem RelIso.cast_refl {α : Type u} {r : ααProp} (h₁ : optParam (α = α) (_ : α = α)) (h₂ : optParam (HEq r r) (_ : 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.trans (RelIso.cast h₁ h₂) (RelIso.cast h₁' h₂') = RelIso.cast (_ : α = γ) (_ : HEq r t)
          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
          @[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) :
          (RelIso.toRelEmbedding (RelIso.symm { toEquiv := f, map_rel_iff' := o })).toEmbedding = ↑(Equiv.symm f)
          @[simp]
          theorem RelIso.apply_symm_apply {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (e : r ≃r s) (x : β) :
          (RelIso.toRelEmbedding e).toEmbedding ((RelIso.toRelEmbedding (RelIso.symm e)).toEmbedding x) = x
          @[simp]
          theorem RelIso.symm_apply_apply {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (e : r ≃r s) (x : α) :
          (RelIso.toRelEmbedding (RelIso.symm e)).toEmbedding ((RelIso.toRelEmbedding e).toEmbedding 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 ((RelIso.toRelEmbedding (RelIso.symm e)).toEmbedding y) s ((RelIso.toRelEmbedding e).toEmbedding x) y
          theorem RelIso.symm_apply_rel {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (e : r ≃r s) {x : β} {y : α} :
          r ((RelIso.toRelEmbedding (RelIso.symm e)).toEmbedding x) y s x ((RelIso.toRelEmbedding e).toEmbedding y)
          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 : α} :
          (RelIso.toRelEmbedding f).toEmbedding a = (RelIso.toRelEmbedding f).toEmbedding 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
          • RelIso.preimage f s = { toEquiv := f, map_rel_iff' := (_ : ∀ {a b : α}, s (f a) (f b) s (f a) (f b)) }
          instance RelIso.IsWellOrder.preimage {β : Type u_1} {α : Type u} (r : ααProp) [inst : IsWellOrder α r] (f : β α) :
          IsWellOrder β (f ⁻¹'o r)
          Equations
          instance RelIso.IsWellOrder.ulift {α : Type u} (r : ααProp) [inst : IsWellOrder α r] :
          IsWellOrder (ULift α) (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.toEmbedding) (a : α) :
          (RelIso.toRelEmbedding (RelIso.ofSurjective f H)).toEmbedding a = f.toEmbedding a
          noncomputable def RelIso.ofSurjective {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) (H : Function.Surjective f.toEmbedding) :
          r ≃r s

          A surjective relation embedding is a relation isomorphism.

          Equations
          • One or more equations did not get rendered due to their size.
          def RelIso.sumLexCongr {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {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₁≃r s₁ and r₂ ≃r s₂≃r s₂, construct a relation isomorphism for the lexicographic orders on the sum.

          Equations
          • One or more equations did not get rendered due to their size.
          def RelIso.prodLexCongr {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {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₁≃r s₁ and r₂ ≃r s₂≃r s₂, construct a relation isomorphism for the lexicographic orders on the product.

          Equations
          • One or more equations did not get rendered due to their size.
          def RelIso.relIsoOfIsEmpty {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [inst : IsEmpty α] [inst : IsEmpty β] :
          r ≃r s

          Two relations on empty types are isomorphic.

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

          Two irreflexive relations on a unique type are isomorphic.

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

          Two reflexive relations on a unique type are isomorphic.

          Equations