Documentation

Mathlib.Data.Rel

Relations as sets of pairs #

This file provides API to regard relations between α and β as sets of pairs Set (α × β).

This is in particular useful in the study of uniform spaces, which are topological spaces equipped with a uniformity, namely a filter of pairs α × α whose elements can be viewed as "proximity" relations.

Main declarations #

Implementation notes #

There is tension throughout the library between considering relations between α and β simply as α → β → Prop, or as a bundled object SetRel α β with dedicated operations and API.

The former approach is used almost everywhere as it is very lightweight and has arguably native support from core Lean features, but it cracks at the seams whenever one starts talking about operations on relations. For example:

The latter approach is embodied by SetRel α β, with dedicated notation like for composition.

Previously, SetRel suffered from the leakage of its definition as

def SetRel (α β : Type*) := α → β → Prop

The fact that SetRel wasn't an abbrev confuses automation. But simply making it an abbrev would have killed the point of having a separate less see-through type to perform relation operations on, so we instead redefined

def SetRel (α β : Type*) := Set (α × β) → Prop

This extra level of indirection guides automation correctly and prevents (some kinds of) leakage.

Simultaneously, uniform spaces need a theory of relations on a type α as elements of Set (α × α), and the new definition of SetRel fulfills this role quite well.

@[reducible, inline]
abbrev SetRel (α : Type u_6) (β : Type u_7) :
Type (max u_7 u_6)

A relation on α and β, aka a set-valued function, aka a partial multifunction.

We represent them as sets due to how relations are used in the context of uniform spaces.

Equations
Instances For

    Notation for apply a relation R : SetRel α β to a : α, b : β, scoped to the SetRel namespace.

    Since SetRel α β := Set (α × β), a ~[R] b is simply notation for (a, b) ∈ R, but this should be considered an implementation detail.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      def SetRel.inv {α : Type u_1} {β : Type u_2} (R : SetRel α β) :
      SetRel β α

      The inverse relation : R.inv x y ↔ R y x. Note that this is not a groupoid inverse.

      Equations
      Instances For
        @[simp]
        theorem SetRel.mem_inv {α : Type u_1} {β : Type u_2} {R : SetRel α β} {a : α} {b : β} :
        (b, a) R.inv (a, b) R
        @[deprecated SetRel.mem_inv (since := "2025-07-06")]
        theorem SetRel.inv_def {α : Type u_1} {β : Type u_2} {R : SetRel α β} {a : α} {b : β} :
        (b, a) R.inv (a, b) R

        Alias of SetRel.mem_inv.

        @[simp]
        theorem SetRel.inv_inv {α : Type u_1} {β : Type u_2} {R : SetRel α β} :
        R.inv.inv = R
        theorem SetRel.inv_mono {α : Type u_1} {β : Type u_2} {R₁ R₂ : SetRel α β} (h : R₁ R₂) :
        R₁.inv R₂.inv
        @[simp]
        theorem SetRel.inv_empty {α : Type u_1} {β : Type u_2} :
        @[simp]
        theorem SetRel.inv_univ {α : Type u_1} {β : Type u_2} :
        @[deprecated SetRel.inv_empty (since := "2025-07-06")]
        theorem SetRel.inv_bot {α : Type u_1} {β : Type u_2} :

        Alias of SetRel.inv_empty.

        def SetRel.dom {α : Type u_1} {β : Type u_2} (R : SetRel α β) :
        Set α

        Domain of a relation.

        Equations
        Instances For
          def SetRel.cod {α : Type u_1} {β : Type u_2} (R : SetRel α β) :
          Set β

          Codomain of a relation, aka range.

          Equations
          Instances For
            @[deprecated SetRel.cod (since := "2025-07-06")]
            def SetRel.codom {α : Type u_1} {β : Type u_2} (R : SetRel α β) :
            Set β

            Alias of SetRel.cod.


            Codomain of a relation, aka range.

            Equations
            Instances For
              @[simp]
              theorem SetRel.mem_dom {α : Type u_1} {β : Type u_2} {R : SetRel α β} {a : α} :
              a R.dom ∃ (b : β), (a, b) R
              @[simp]
              theorem SetRel.mem_cod {α : Type u_1} {β : Type u_2} {R : SetRel α β} {b : β} :
              b R.cod ∃ (a : α), (a, b) R
              theorem SetRel.dom_mono {α : Type u_1} {β : Type u_2} {R₁ R₂ : SetRel α β} (h : R₁ R₂) :
              R₁.dom R₂.dom
              theorem SetRel.cod_mono {α : Type u_1} {β : Type u_2} {R₁ R₂ : SetRel α β} (h : R₁ R₂) :
              R₁.cod R₂.cod
              @[simp]
              theorem SetRel.dom_empty {α : Type u_1} {β : Type u_2} :
              @[simp]
              theorem SetRel.cod_empty {α : Type u_1} {β : Type u_2} :
              @[simp]
              theorem SetRel.dom_univ {α : Type u_1} {β : Type u_2} [Nonempty β] :
              @[simp]
              theorem SetRel.cod_univ {α : Type u_1} {β : Type u_2} [Nonempty α] :
              @[simp]
              theorem SetRel.cod_inv {α : Type u_1} {β : Type u_2} {R : SetRel α β} :
              R.inv.cod = R.dom
              @[simp]
              theorem SetRel.dom_inv {α : Type u_1} {β : Type u_2} {R : SetRel α β} :
              R.inv.dom = R.cod
              @[deprecated SetRel.cod_inv (since := "2025-07-06")]
              theorem SetRel.codom_inv {α : Type u_1} {β : Type u_2} {R : SetRel α β} :
              R.inv.cod = R.dom

              Alias of SetRel.cod_inv.

              def SetRel.id {α : Type u_1} :
              SetRel α α

              The identity relation.

              Equations
              Instances For
                @[simp]
                theorem SetRel.mem_id {α : Type u_1} {a₁ a₂ : α} :
                (a₁, a₂) SetRel.id a₁ = a₂
                def SetRel.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (R : SetRel α β) (S : SetRel β γ) :
                SetRel α γ

                Composition of relation.

                Note that this follows the CategoryTheory order of arguments.

                Equations
                Instances For

                  Composition of relation.

                  Note that this follows the CategoryTheory order of arguments.

                  Equations
                  Instances For
                    @[simp]
                    theorem SetRel.mem_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {R : SetRel α β} {S : SetRel β γ} {a : α} {c : γ} :
                    (a, c) R.comp S ∃ (b : β), (a, b) R (b, c) S
                    theorem SetRel.prodMk_mem_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {R : SetRel α β} {S : SetRel β γ} {a : α} {b : β} {c : γ} (hab : (a, b) R) (hbc : (b, c) S) :
                    (a, c) R.comp S
                    theorem SetRel.comp_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (R : SetRel α β) (S : SetRel β γ) (t : SetRel γ δ) :
                    (R.comp S).comp t = R.comp (S.comp t)
                    @[simp]
                    theorem SetRel.comp_id {α : Type u_1} {β : Type u_2} (R : SetRel α β) :
                    @[simp]
                    theorem SetRel.id_comp {α : Type u_1} {β : Type u_2} (R : SetRel α β) :
                    @[simp]
                    theorem SetRel.inv_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (R : SetRel α β) (S : SetRel β γ) :
                    (R.comp S).inv = S.inv.comp R.inv
                    @[simp]
                    theorem SetRel.comp_empty {α : Type u_1} {β : Type u_2} {γ : Type u_3} (R : SetRel α β) :
                    @[simp]
                    theorem SetRel.empty_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (S : SetRel β γ) :
                    @[simp]
                    theorem SetRel.comp_univ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (R : SetRel α β) :
                    R.comp Set.univ = {(a, _c) : α × γ | a R.dom}
                    @[simp]
                    theorem SetRel.univ_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (S : SetRel β γ) :
                    comp Set.univ S = {(_b, c) : α × γ | c S.cod}
                    theorem SetRel.comp_iUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_5} (R : SetRel α β) (S : ιSetRel β γ) :
                    R.comp (⋃ (i : ι), S i) = ⋃ (i : ι), R.comp (S i)
                    theorem SetRel.iUnion_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_5} (R : ιSetRel α β) (S : SetRel β γ) :
                    comp (⋃ (i : ι), R i) S = ⋃ (i : ι), (R i).comp S
                    theorem SetRel.comp_sUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} (R : SetRel α β) (𝒮 : Set (SetRel β γ)) :
                    R.comp (⋃₀ 𝒮) = S𝒮, R.comp S
                    theorem SetRel.sUnion_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} ( : Set (SetRel α β)) (S : SetRel β γ) :
                    comp (⋃₀ ) S = R, R.comp S
                    theorem SetRel.comp_subset_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {R₁ R₂ : SetRel α β} {S₁ S₂ : SetRel β γ} (hR : R₁ R₂) (hS : S₁ S₂) :
                    R₁.comp S₁ R₂.comp S₂
                    theorem SetRel.comp_subset_comp_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {R₁ R₂ : SetRel α β} {S : SetRel β γ} (hR : R₁ R₂) :
                    R₁.comp S R₂.comp S
                    theorem SetRel.comp_subset_comp_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {R : SetRel α β} {S₁ S₂ : SetRel β γ} (hS : S₁ S₂) :
                    R.comp S₁ R.comp S₂
                    theorem Monotone.relComp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_6} [Preorder ι] {f : ιSetRel α β} {g : ιSetRel β γ} (hf : Monotone f) (hg : Monotone g) :
                    Monotone fun (x : ι) => (f x).comp (g x)
                    theorem SetRel.prod_comp_prod_of_inter_nonempty {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t₁ t₂ : Set β} (ht : (t₁ t₂).Nonempty) (s : Set α) (u : Set γ) :
                    comp (s ×ˢ t₁) (t₂ ×ˢ u) = s ×ˢ u
                    theorem SetRel.prod_comp_prod_of_disjoint {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t₁ t₂ : Set β} (ht : Disjoint t₁ t₂) (s : Set α) (u : Set γ) :
                    comp (s ×ˢ t₁) (t₂ ×ˢ u) =
                    theorem SetRel.prod_comp_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} (s : Set α) (t₁ t₂ : Set β) (u : Set γ) [Decidable (Disjoint t₁ t₂)] :
                    comp (s ×ˢ t₁) (t₂ ×ˢ u) = if Disjoint t₁ t₂ then else s ×ˢ u
                    @[deprecated SetRel.comp_univ (since := "2025-07-06")]
                    theorem SetRel.comp_right_top {α : Type u_1} {β : Type u_2} {γ : Type u_3} (R : SetRel α β) :
                    R.comp Set.univ = {(a, _c) : α × γ | a R.dom}

                    Alias of SetRel.comp_univ.

                    @[deprecated SetRel.univ_comp (since := "2025-07-06")]
                    theorem SetRel.comp_left_top {α : Type u_1} {β : Type u_2} {γ : Type u_3} (S : SetRel β γ) :
                    comp Set.univ S = {(_b, c) : α × γ | c S.cod}

                    Alias of SetRel.univ_comp.

                    def SetRel.image {α : Type u_1} {β : Type u_2} (R : SetRel α β) (s : Set α) :
                    Set β

                    Image of a set under a relation.

                    Equations
                    Instances For
                      def SetRel.preimage {α : Type u_1} {β : Type u_2} (R : SetRel α β) (t : Set β) :
                      Set α

                      Preimage of a set t under a relation R. Same as the image of t under R.inv.

                      Equations
                      Instances For
                        @[simp]
                        theorem SetRel.mem_image {α : Type u_1} {β : Type u_2} {R : SetRel α β} {s : Set α} {b : β} :
                        b R.image s as, (a, b) R
                        @[simp]
                        theorem SetRel.mem_preimage {α : Type u_1} {β : Type u_2} {R : SetRel α β} {t : Set β} {a : α} :
                        a R.preimage t bt, (a, b) R
                        theorem SetRel.image_subset_image {α : Type u_1} {β : Type u_2} {R : SetRel α β} {s₁ s₂ : Set α} (hs : s₁ s₂) :
                        R.image s₁ R.image s₂
                        theorem SetRel.preimage_subset_preimage {α : Type u_1} {β : Type u_2} {R : SetRel α β} {t₁ t₂ : Set β} (ht : t₁ t₂) :
                        R.preimage t₁ R.preimage t₂
                        @[simp]
                        theorem SetRel.image_inv {α : Type u_1} {β : Type u_2} (R : SetRel α β) (t : Set β) :
                        @[simp]
                        theorem SetRel.preimage_inv {α : Type u_1} {β : Type u_2} (R : SetRel α β) (s : Set α) :
                        theorem SetRel.image_mono {α : Type u_1} {β : Type u_2} {R : SetRel α β} :
                        theorem SetRel.preimage_mono {α : Type u_1} {β : Type u_2} {R : SetRel α β} :
                        @[simp]
                        theorem SetRel.image_empty_right {α : Type u_1} {β : Type u_2} {R : SetRel α β} :
                        @[simp]
                        theorem SetRel.preimage_empty_right {α : Type u_1} {β : Type u_2} {R : SetRel α β} :
                        @[simp]
                        theorem SetRel.image_univ_right {α : Type u_1} {β : Type u_2} {R : SetRel α β} :
                        @[simp]
                        theorem SetRel.preimage_univ_right {α : Type u_1} {β : Type u_2} {R : SetRel α β} :
                        theorem SetRel.image_inter_subset {α : Type u_1} {β : Type u_2} (R : SetRel α β) {s₁ s₂ : Set α} :
                        R.image (s₁ s₂) R.image s₁ R.image s₂
                        @[deprecated SetRel.image_inter_subset (since := "2025-07-06")]
                        theorem SetRel.preimage_top {α : Type u_1} {β : Type u_2} (R : SetRel α β) {s₁ s₂ : Set α} :
                        R.image (s₁ s₂) R.image s₁ R.image s₂

                        Alias of SetRel.image_inter_subset.

                        theorem SetRel.preimage_inter_subset {α : Type u_1} {β : Type u_2} (R : SetRel α β) {t₁ t₂ : Set β} :
                        R.preimage (t₁ t₂) R.preimage t₁ R.preimage t₂
                        @[deprecated SetRel.preimage_inter_subset (since := "2025-07-06")]
                        theorem SetRel.image_eq_dom_of_codomain_subset {α : Type u_1} {β : Type u_2} (R : SetRel α β) {t₁ t₂ : Set β} :
                        R.preimage (t₁ t₂) R.preimage t₁ R.preimage t₂

                        Alias of SetRel.preimage_inter_subset.

                        theorem SetRel.image_union {α : Type u_1} {β : Type u_2} (R : SetRel α β) (s₁ s₂ : Set α) :
                        R.image (s₁ s₂) = R.image s₁ R.image s₂
                        @[deprecated SetRel.image_union (since := "2025-07-06")]
                        theorem SetRel.preimage_eq_codom_of_domain_subset {α : Type u_1} {β : Type u_2} (R : SetRel α β) (s₁ s₂ : Set α) :
                        R.image (s₁ s₂) = R.image s₁ R.image s₂

                        Alias of SetRel.image_union.

                        theorem SetRel.preimage_union {α : Type u_1} {β : Type u_2} (R : SetRel α β) (t₁ t₂ : Set β) :
                        R.preimage (t₁ t₂) = R.preimage t₁ R.preimage t₂
                        @[simp]
                        theorem SetRel.image_id {α : Type u_1} (s : Set α) :
                        @[simp]
                        theorem SetRel.preimage_id {α : Type u_1} (s : Set α) :
                        theorem SetRel.image_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (R : SetRel α β) (S : SetRel β γ) (s : Set α) :
                        (R.comp S).image s = S.image (R.image s)
                        theorem SetRel.preimage_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (R : SetRel α β) (S : SetRel β γ) (u : Set γ) :
                        (R.comp S).preimage u = R.preimage (S.preimage u)
                        @[simp]
                        theorem SetRel.image_empty_left {α : Type u_1} {β : Type u_2} (s : Set α) :
                        @[simp]
                        theorem SetRel.preimage_empty_left {α : Type u_1} {β : Type u_2} (t : Set β) :
                        @[deprecated SetRel.preimage_empty_left (since := "2025-07-06")]
                        theorem SetRel.preimage_bot {α : Type u_1} {β : Type u_2} (t : Set β) :

                        Alias of SetRel.preimage_empty_left.

                        @[simp]
                        theorem SetRel.image_univ_left {α : Type u_1} {β : Type u_2} {s : Set α} (hs : s.Nonempty) :
                        @[simp]
                        theorem SetRel.preimage_univ_left {α : Type u_1} {β : Type u_2} {t : Set β} (ht : t.Nonempty) :
                        theorem SetRel.image_eq_cod_of_dom_subset {α : Type u_1} {β : Type u_2} {R : SetRel α β} {t : Set β} (h : R.cod t) :
                        R.preimage t = R.dom
                        theorem SetRel.preimage_eq_dom_of_cod_subset {α : Type u_1} {β : Type u_2} {R : SetRel α β} {t : Set β} (h : R.cod t) :
                        R.preimage t = R.dom
                        @[simp]
                        theorem SetRel.image_inter_dom {α : Type u_1} {β : Type u_2} (R : SetRel α β) (s : Set α) :
                        R.image (s R.dom) = R.image s
                        @[simp]
                        theorem SetRel.preimage_inter_cod {α : Type u_1} {β : Type u_2} (R : SetRel α β) (t : Set β) :
                        R.preimage (t R.cod) = R.preimage t
                        @[deprecated SetRel.preimage_inter_cod (since := "2025-07-06")]
                        theorem SetRel.preimage_inter_codom_eq {α : Type u_1} {β : Type u_2} (R : SetRel α β) (t : Set β) :
                        R.preimage (t R.cod) = R.preimage t

                        Alias of SetRel.preimage_inter_cod.

                        theorem SetRel.inter_dom_subset_preimage_image {α : Type u_1} {β : Type u_2} {R : SetRel α β} {s : Set α} :
                        s R.dom R.preimage (R.image s)
                        theorem SetRel.inter_cod_subset_image_preimage {α : Type u_1} {β : Type u_2} {R : SetRel α β} {t : Set β} :
                        t R.cod R.image (R.preimage t)
                        @[deprecated SetRel.inter_cod_subset_image_preimage (since := "2025-07-06")]
                        theorem SetRel.image_preimage_subset_inter_codom {α : Type u_1} {β : Type u_2} {R : SetRel α β} {t : Set β} :
                        t R.cod R.image (R.preimage t)

                        Alias of SetRel.inter_cod_subset_image_preimage.

                        def SetRel.core {α : Type u_1} {β : Type u_2} (R : SetRel α β) (t : Set β) :
                        Set α

                        Core of a set S : Set β w.R.t R : SetRel α β is the set of x : α that are related only to elements of S. Other generalization of Function.preimage.

                        Equations
                        Instances For
                          @[simp]
                          theorem SetRel.mem_core {α : Type u_1} {β : Type u_2} {R : SetRel α β} {t : Set β} {a : α} :
                          a R.core t ∀ ⦃b : β⦄, (a, b) Rb t
                          theorem SetRel.core_subset_core {α : Type u_1} {β : Type u_2} {R : SetRel α β} {t₁ t₂ : Set β} (ht : t₁ t₂) :
                          R.core t₁ R.core t₂
                          theorem SetRel.core_mono {α : Type u_1} {β : Type u_2} {R : SetRel α β} :
                          theorem SetRel.core_inter {α : Type u_1} {β : Type u_2} (R : SetRel α β) (t₁ t₂ : Set β) :
                          R.core (t₁ t₂) = R.core t₁ R.core t₂
                          theorem SetRel.core_union_subset {α : Type u_1} {β : Type u_2} {R : SetRel α β} {t₁ t₂ : Set β} :
                          R.core t₁ R.core t₂ R.core (t₁ t₂)
                          @[simp]
                          theorem SetRel.core_univ {α : Type u_1} {β : Type u_2} {R : SetRel α β} :
                          @[simp]
                          theorem SetRel.core_id {β : Type u_2} (t : Set β) :
                          theorem SetRel.core_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (R : SetRel α β) (S : SetRel β γ) (u : Set γ) :
                          (R.comp S).core u = R.core (S.core u)
                          theorem SetRel.image_subset_iff {α : Type u_1} {β : Type u_2} {R : SetRel α β} {s : Set α} {t : Set β} :
                          R.image s t s R.core t
                          theorem SetRel.image_core_gc {α : Type u_1} {β : Type u_2} {R : SetRel α β} :
                          def SetRel.restrictDomain {α : Type u_1} {β : Type u_2} (R : SetRel α β) (s : Set α) :
                          SetRel (↑s) β

                          Restrict the domain of a relation to a subtype.

                          Equations
                          Instances For

                            Reflexive relations #

                            @[reducible, inline]
                            abbrev SetRel.IsRefl {α : Type u_1} (R : SetRel α α) :

                            A relation R is reflexive if a ~[R] a.

                            Equations
                            Instances For
                              theorem SetRel.refl {α : Type u_1} (R : SetRel α α) [R.IsRefl] (a : α) :
                              (a, a) R
                              theorem SetRel.rfl {α : Type u_1} (R : SetRel α α) {a : α} [R.IsRefl] :
                              (a, a) R
                              theorem SetRel.id_subset {α : Type u_1} {R : SetRel α α} [R.IsRefl] :
                              theorem SetRel.id_subset_iff {α : Type u_1} {R : SetRel α α} :
                              instance SetRel.isRefl_inter {α : Type u_1} {R₁ R₂ : SetRel α α} [R₁.IsRefl] [R₂.IsRefl] :
                              (R₁ R₂).IsRefl
                              theorem SetRel.IsRefl.sInter {α : Type u_1} { : Set (SetRel α α)} (hℛ : R, R.IsRefl) :
                              instance SetRel.isRefl_iInter {α : Type u_1} {ι : Sort u_5} {R : ιSetRel α α} [∀ (i : ι), (R i).IsRefl] :
                              SetRel.IsRefl (⋂ (i : ι), R i)
                              instance SetRel.isRefl_preimage {α : Type u_1} {β : Type u_2} {R : SetRel α α} {f : βα} [R.IsRefl] :
                              theorem SetRel.isRefl_mono {α : Type u_1} {R₁ R₂ : SetRel α α} [R₁.IsRefl] (hR : R₁ R₂) :
                              R₂.IsRefl
                              theorem SetRel.left_subset_comp {α : Type u_1} {β : Type u_2} {S : SetRel β β} {R : SetRel α β} [S.IsRefl] :
                              R R.comp S
                              theorem SetRel.right_subset_comp {α : Type u_1} {β : Type u_2} {R : SetRel α α} [R.IsRefl] {S : SetRel α β} :
                              S R.comp S
                              theorem SetRel.subset_iterate_comp {α : Type u_1} {β : Type u_2} {R : SetRel α α} [R.IsRefl] {S : SetRel α β} {n : } :
                              S (fun (x : SetRel α β) => R.comp x)^[n] S
                              theorem SetRel.exists_eq_singleton_of_prod_subset_id {α : Type u_1} {s t : Set α} (hs : s.Nonempty) (ht : t.Nonempty) (hst : s ×ˢ t SetRel.id) :
                              ∃ (x : α), s = {x} t = {x}

                              Symmetric relations #

                              @[reducible, inline]
                              abbrev SetRel.IsSymm {α : Type u_1} (R : SetRel α α) :

                              A relation R is symmetric if a ~[R] b ↔ b ~[R] a.

                              Equations
                              Instances For
                                theorem SetRel.symm {α : Type u_1} (R : SetRel α α) {a b : α} [R.IsSymm] (hab : (a, b) R) :
                                (b, a) R
                                theorem SetRel.comm {α : Type u_1} (R : SetRel α α) {a b : α} [R.IsSymm] :
                                (a, b) R (b, a) R
                                @[simp]
                                theorem SetRel.inv_eq_self {α : Type u_1} (R : SetRel α α) [R.IsSymm] :
                                R.inv = R
                                theorem SetRel.inv_eq_self_iff {α : Type u_1} {R : SetRel α α} :
                                R.inv = R R.IsSymm
                                instance SetRel.instIsSymmInv {α : Type u_1} {R : SetRel α α} [R.IsSymm] :
                                instance SetRel.isSymm_inter {α : Type u_1} {R₁ R₂ : SetRel α α} [R₁.IsSymm] [R₂.IsSymm] :
                                (R₁ R₂).IsSymm
                                theorem SetRel.IsSymm.sInter {α : Type u_1} { : Set (SetRel α α)} (hℛ : R, R.IsSymm) :
                                instance SetRel.isSymm_iInter {α : Type u_1} {ι : Sort u_5} {R : ιSetRel α α} [∀ (i : ι), (R i).IsSymm] :
                                SetRel.IsSymm (⋂ (i : ι), R i)
                                instance SetRel.isSymm_preimage {α : Type u_1} {β : Type u_2} {R : SetRel α α} {f : βα} [R.IsSymm] :
                                instance SetRel.isSymm_comp_inv {α : Type u_1} {R : SetRel α α} :
                                instance SetRel.isSymm_inv_comp {α : Type u_1} {R : SetRel α α} :
                                instance SetRel.isSymm_comp_self {α : Type u_1} {R : SetRel α α} [R.IsSymm] :
                                (R.comp R).IsSymm
                                def SetRel.symmetrize {α : Type u_1} (R : SetRel α α) :
                                SetRel α α

                                The maximal symmetric relation contained in a given relation.

                                Equations
                                Instances For
                                  instance SetRel.isSymm_symmetrize {α : Type u_1} {R : SetRel α α} :
                                  theorem SetRel.symmetrize_subset_self {α : Type u_1} {R : SetRel α α} :
                                  theorem SetRel.symmetrize_subset_inv {α : Type u_1} {R : SetRel α α} :
                                  theorem SetRel.subset_symmetrize {α : Type u_1} {R S : SetRel α α} :
                                  theorem SetRel.symmetrize_mono {α : Type u_1} {R₁ R₂ : SetRel α α} (h : R₁ R₂) :

                                  Transitive relations #

                                  @[reducible, inline]
                                  abbrev SetRel.IsTrans {α : Type u_1} (R : SetRel α α) :

                                  A relation R is transitive if a ~[R] b and b ~[R] c together imply a ~[R] c.

                                  Equations
                                  Instances For
                                    theorem SetRel.trans {α : Type u_1} (R : SetRel α α) {a b c : α} [R.IsTrans] (hab : (a, b) R) (hbc : (b, c) R) :
                                    (a, c) R
                                    instance SetRel.instIsTransSetOfProdMatch_1PropOfIsTrans {α : Type u_1} {R : ααProp} [IsTrans α R] :
                                    SetRel.IsTrans {(a, b) : α × α | R a b}
                                    theorem SetRel.comp_subset_self {α : Type u_1} {R : SetRel α α} [R.IsTrans] :
                                    R.comp R R
                                    theorem SetRel.comp_eq_self {α : Type u_1} {R : SetRel α α} [R.IsRefl] [R.IsTrans] :
                                    R.comp R = R
                                    theorem SetRel.isTrans_iff_comp_subset_self {α : Type u_1} {R : SetRel α α} :
                                    instance SetRel.isTrans_singleton {α : Type u_1} (x : α × α) :
                                    instance SetRel.isTrans_inter {α : Type u_1} {R₁ R₂ : SetRel α α} [R₁.IsTrans] [R₂.IsTrans] :
                                    (R₁ R₂).IsTrans
                                    theorem SetRel.IsTrans.sInter {α : Type u_1} { : Set (SetRel α α)} (hℛ : R, R.IsTrans) :
                                    instance SetRel.isTrans_iInter {α : Type u_1} {ι : Sort u_5} {R : ιSetRel α α} [∀ (i : ι), (R i).IsTrans] :
                                    SetRel.IsTrans (⋂ (i : ι), R i)
                                    instance SetRel.isTrans_preimage {α : Type u_1} {β : Type u_2} {R : SetRel α α} {f : βα} [R.IsTrans] :
                                    instance SetRel.isTrans_symmetrize {α : Type u_1} {R : SetRel α α} [R.IsTrans] :
                                    @[reducible, inline]
                                    abbrev SetRel.IsIrrefl {α : Type u_1} (R : SetRel α α) :

                                    A relation R is irreflexive if ¬ a ~[R] a.

                                    Equations
                                    Instances For
                                      theorem SetRel.irrefl {α : Type u_1} (R : SetRel α α) (a : α) [R.IsIrrefl] :
                                      (a, a)R
                                      instance SetRel.instIsIrreflSetOfProdMatch_1PropOfIsIrrefl {α : Type u_1} {R : ααProp} [IsIrrefl α R] :
                                      SetRel.IsIrrefl {(a, b) : α × α | R a b}
                                      @[reducible, inline]
                                      abbrev SetRel.IsWellFounded {α : Type u_1} (R : SetRel α α) :

                                      A relation R on a type α is well-founded if all elements of α are accessible within R.

                                      Equations
                                      Instances For
                                        @[reducible, inline]
                                        abbrev SetRel.Hom {α : Type u_1} {β : Type u_2} (R : SetRel α α) (S : SetRel β β) :
                                        Type (max u_1 u_2)

                                        A relation homomorphism with respect to a given pair of relations R and S s is a function f : α → β such that a ~[R] b → f a ~[s] f b.

                                        Equations
                                        Instances For
                                          def Function.graph {α : Type u_1} {β : Type u_2} (f : αβ) :
                                          SetRel α β

                                          The graph of a function as a relation.

                                          Equations
                                          Instances For
                                            @[simp]
                                            theorem Function.mem_graph {α : Type u_1} {β : Type u_2} {f : αβ} {a : α} {b : β} :
                                            (a, b) graph f f a = b
                                            @[deprecated Function.mem_graph (since := "2025-07-06")]
                                            theorem Function.graph_def {α : Type u_1} {β : Type u_2} {f : αβ} {a : α} {b : β} :
                                            (a, b) graph f f a = b

                                            Alias of Function.mem_graph.

                                            theorem Function.graph_injective {α : Type u_1} {β : Type u_2} :
                                            @[simp]
                                            theorem Function.graph_inj {α : Type u_1} {β : Type u_2} {f g : αβ} :
                                            graph f = graph g f = g
                                            @[simp]
                                            theorem Function.graph_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : βγ) (g : αβ) :
                                            graph (f g) = (graph g).comp (graph f)
                                            theorem Equiv.graph_inv {α : Type u_1} {β : Type u_2} (f : α β) :
                                            theorem SetRel.exists_graph_eq_iff {α : Type u_1} {β : Type u_2} (R : SetRel α β) :
                                            (∃! f : αβ, Function.graph f = R) ∀ (a : α), ∃! b : β, (a, b) R
                                            @[deprecated SetRel.exists_graph_eq_iff (since := "2025-07-06")]
                                            theorem SetRelation.is_graph_iff {α : Type u_1} {β : Type u_2} (R : SetRel α β) :
                                            (∃! f : αβ, Function.graph f = R) ∀ (a : α), ∃! b : β, (a, b) R

                                            Alias of SetRel.exists_graph_eq_iff.

                                            theorem Set.image_eq {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
                                            theorem Set.preimage_eq {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set β) :
                                            theorem Set.preimage_eq_core {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set β) :
                                            @[reducible, inline]
                                            abbrev Rel (α : Type u_6) (β : Type u_7) :
                                            Type (max u_6 u_7)

                                            A shorthand for α → β → Prop.

                                            Consider using SetRel instead if you want extra API for relations.

                                            Equations
                                            Instances For