Documentation

Mathlib.Data.Rel

Relations #

This file defines bundled relations. A relation between α and β is a function α → β → Prop. Relations are also known as set-valued functions, or partial multifunctions.

Main declarations #

def Rel (α : Type u_4) (β : Type u_5) :
Type (max u_4 u_5)

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

Equations
Instances For
    instance instCompleteLatticeRel {α : Type u_1} {β : Type u_2} :
    Equations
    • instCompleteLatticeRel = let_fun this := inferInstance; this
    instance instInhabitedRel {α : Type u_1} {β : Type u_2} :
    Inhabited (Rel α β)
    Equations
    • instInhabitedRel = let_fun this := inferInstance; this
    theorem Rel.ext {α : Type u_1} {β : Type u_2} {r : Rel α β} {s : Rel α β} :
    (∀ (a : α), r a = s a)r = s
    def Rel.inv {α : Type u_1} {β : Type u_2} (r : Rel α β) :
    Rel β α

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

    Equations
    Instances For
      theorem Rel.inv_def {α : Type u_1} {β : Type u_2} (r : Rel α β) (x : α) (y : β) :
      Rel.inv r y x r x y
      theorem Rel.inv_inv {α : Type u_1} {β : Type u_2} (r : Rel α β) :
      def Rel.dom {α : Type u_1} {β : Type u_2} (r : Rel α β) :
      Set α

      Domain of a relation

      Equations
      • Rel.dom r = {x : α | ∃ (y : β), r x y}
      Instances For
        theorem Rel.dom_mono {α : Type u_1} {β : Type u_2} {r : Rel α β} {s : Rel α β} (h : r s) :
        def Rel.codom {α : Type u_1} {β : Type u_2} (r : Rel α β) :
        Set β

        Codomain aka range of a relation

        Equations
        Instances For
          theorem Rel.codom_inv {α : Type u_1} {β : Type u_2} (r : Rel α β) :
          theorem Rel.dom_inv {α : Type u_1} {β : Type u_2} (r : Rel α β) :
          def Rel.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (r : Rel α β) (s : Rel β γ) :
          Rel α γ

          Composition of relation; note that it follows the CategoryTheory/ order of arguments.

          Equations
          Instances For
            theorem Rel.comp_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (r : Rel α β) (s : Rel β γ) (t : Rel γ δ) :
            @[simp]
            theorem Rel.comp_right_id {α : Type u_1} {β : Type u_2} (r : Rel α β) :
            Rel.comp r Eq = r
            @[simp]
            theorem Rel.comp_left_id {α : Type u_1} {β : Type u_2} (r : Rel α β) :
            Rel.comp Eq r = r
            @[simp]
            theorem Rel.comp_right_bot {α : Type u_1} {β : Type u_2} {γ : Type u_3} (r : Rel α β) :
            @[simp]
            theorem Rel.comp_left_bot {α : Type u_1} {β : Type u_2} {γ : Type u_3} (r : Rel α β) :
            @[simp]
            theorem Rel.comp_right_top {α : Type u_1} {β : Type u_2} {γ : Type u_3} (r : Rel α β) :
            Rel.comp r = fun (x : α) (x_1 : γ) => x Rel.dom r
            @[simp]
            theorem Rel.comp_left_top {α : Type u_1} {β : Type u_2} {γ : Type u_3} (r : Rel α β) :
            Rel.comp r = fun (x : γ) (y : β) => y Rel.codom r
            theorem Rel.inv_id {α : Type u_1} :
            Rel.inv Eq = Eq
            theorem Rel.inv_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (r : Rel α β) (s : Rel β γ) :
            @[simp]
            theorem Rel.inv_bot {α : Type u_1} {β : Type u_2} :
            @[simp]
            theorem Rel.inv_top {α : Type u_1} {β : Type u_2} :
            def Rel.image {α : Type u_1} {β : Type u_2} (r : Rel α β) (s : Set α) :
            Set β

            Image of a set under a relation

            Equations
            Instances For
              theorem Rel.mem_image {α : Type u_1} {β : Type u_2} (r : Rel α β) (y : β) (s : Set α) :
              y Rel.image r s ∃ x ∈ s, r x y
              theorem Rel.image_subset {α : Type u_1} {β : Type u_2} (r : Rel α β) :
              ((fun (x x_1 : Set α) => x x_1) fun (x x_1 : Set β) => x x_1) (Rel.image r) (Rel.image r)
              theorem Rel.image_mono {α : Type u_1} {β : Type u_2} (r : Rel α β) :
              theorem Rel.image_inter {α : Type u_1} {β : Type u_2} (r : Rel α β) (s : Set α) (t : Set α) :
              theorem Rel.image_union {α : Type u_1} {β : Type u_2} (r : Rel α β) (s : Set α) (t : Set α) :
              @[simp]
              theorem Rel.image_id {α : Type u_1} (s : Set α) :
              Rel.image Eq s = s
              theorem Rel.image_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (r : Rel α β) (s : Rel β γ) (t : Set α) :
              theorem Rel.image_univ {α : Type u_1} {β : Type u_2} (r : Rel α β) :
              Rel.image r Set.univ = Rel.codom r
              @[simp]
              theorem Rel.image_empty {α : Type u_1} {β : Type u_2} (r : Rel α β) :
              @[simp]
              theorem Rel.image_bot {α : Type u_1} {β : Type u_2} (s : Set α) :
              @[simp]
              theorem Rel.image_top {α : Type u_1} {β : Type u_2} {s : Set α} (h : Set.Nonempty s) :
              Rel.image s = Set.univ
              def Rel.preimage {α : Type u_1} {β : Type u_2} (r : Rel α β) (s : Set β) :
              Set α

              Preimage of a set under a relation r. Same as the image of s under r.inv

              Equations
              Instances For
                theorem Rel.mem_preimage {α : Type u_1} {β : Type u_2} (r : Rel α β) (x : α) (s : Set β) :
                x Rel.preimage r s ∃ y ∈ s, r x y
                theorem Rel.preimage_def {α : Type u_1} {β : Type u_2} (r : Rel α β) (s : Set β) :
                Rel.preimage r s = {x : α | ∃ y ∈ s, r x y}
                theorem Rel.preimage_mono {α : Type u_1} {β : Type u_2} (r : Rel α β) {s : Set β} {t : Set β} (h : s t) :
                theorem Rel.preimage_inter {α : Type u_1} {β : Type u_2} (r : Rel α β) (s : Set β) (t : Set β) :
                theorem Rel.preimage_union {α : Type u_1} {β : Type u_2} (r : Rel α β) (s : Set β) (t : Set β) :
                theorem Rel.preimage_id {α : Type u_1} (s : Set α) :
                theorem Rel.preimage_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (r : Rel α β) (s : Rel β γ) (t : Set γ) :
                theorem Rel.preimage_univ {α : Type u_1} {β : Type u_2} (r : Rel α β) :
                Rel.preimage r Set.univ = Rel.dom r
                @[simp]
                theorem Rel.preimage_empty {α : Type u_1} {β : Type u_2} (r : Rel α β) :
                @[simp]
                theorem Rel.preimage_inv {α : Type u_1} {β : Type u_2} (r : Rel α β) (s : Set α) :
                @[simp]
                theorem Rel.preimage_bot {α : Type u_1} {β : Type u_2} (s : Set β) :
                @[simp]
                theorem Rel.preimage_top {α : Type u_1} {β : Type u_2} {s : Set β} (h : Set.Nonempty s) :
                Rel.preimage s = Set.univ
                theorem Rel.image_eq_dom_of_codomain_subset {α : Type u_1} {β : Type u_2} (r : Rel α β) {s : Set β} (h : Rel.codom r s) :
                theorem Rel.preimage_eq_codom_of_domain_subset {α : Type u_1} {β : Type u_2} (r : Rel α β) {s : Set α} (h : Rel.dom r s) :
                theorem Rel.image_inter_dom_eq {α : Type u_1} {β : Type u_2} (r : Rel α β) (s : Set α) :
                @[simp]
                theorem Rel.preimage_inter_codom_eq {α : Type u_1} {β : Type u_2} (r : Rel α β) (s : Set β) :
                theorem Rel.inter_dom_subset_preimage_image {α : Type u_1} {β : Type u_2} (r : Rel α β) (s : Set α) :
                theorem Rel.image_preimage_subset_inter_codom {α : Type u_1} {β : Type u_2} (r : Rel α β) (s : Set β) :
                def Rel.core {α : Type u_1} {β : Type u_2} (r : Rel α β) (s : Set β) :
                Set α

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

                Equations
                Instances For
                  theorem Rel.mem_core {α : Type u_1} {β : Type u_2} (r : Rel α β) (x : α) (s : Set β) :
                  x Rel.core r s ∀ (y : β), r x yy s
                  theorem Rel.core_subset {α : Type u_1} {β : Type u_2} (r : Rel α β) :
                  ((fun (x x_1 : Set β) => x x_1) fun (x x_1 : Set α) => x x_1) (Rel.core r) (Rel.core r)
                  theorem Rel.core_mono {α : Type u_1} {β : Type u_2} (r : Rel α β) :
                  theorem Rel.core_inter {α : Type u_1} {β : Type u_2} (r : Rel α β) (s : Set β) (t : Set β) :
                  Rel.core r (s t) = Rel.core r s Rel.core r t
                  theorem Rel.core_union {α : Type u_1} {β : Type u_2} (r : Rel α β) (s : Set β) (t : Set β) :
                  @[simp]
                  theorem Rel.core_univ {α : Type u_1} {β : Type u_2} (r : Rel α β) :
                  Rel.core r Set.univ = Set.univ
                  theorem Rel.core_id {α : Type u_1} (s : Set α) :
                  Rel.core Eq s = s
                  theorem Rel.core_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (r : Rel α β) (s : Rel β γ) (t : Set γ) :
                  def Rel.restrictDomain {α : Type u_1} {β : Type u_2} (r : Rel α β) (s : Set α) :
                  Rel { x : α // x s } β

                  Restrict the domain of a relation to a subtype.

                  Equations
                  Instances For
                    theorem Rel.image_subset_iff {α : Type u_1} {β : Type u_2} (r : Rel α β) (s : Set α) (t : Set β) :
                    theorem Rel.image_core_gc {α : Type u_1} {β : Type u_2} (r : Rel α β) :
                    def Function.graph {α : Type u_1} {β : Type u_2} (f : αβ) :
                    Rel α β

                    The graph of a function as a relation.

                    Equations
                    Instances For
                      @[simp]
                      theorem Function.graph_def {α : Type u_1} {β : Type u_2} (f : αβ) (x : α) (y : β) :
                      Function.graph f x y f x = y
                      theorem Function.graph_id {α : Type u_1} :
                      theorem Function.graph_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : βγ} {g : αβ} :
                      theorem Equiv.graph_inv {α : Type u_1} {β : Type u_2} (f : α β) :
                      theorem Relation.is_graph_iff {α : Type u_1} {β : Type u_2} (r : Rel α β) :
                      (∃! (f : αβ), Function.graph f = r) ∀ (x : α), ∃! (y : β), r x y
                      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 β) :