Documentation

Mathlib.Logic.Relation

Relation closures #

This file defines the reflexive, transitive, reflexive transitive and equivalence closures of relations and proves some basic results on them.

Note that this is about unbundled relations, that is terms of types of the form α → β → Prop. For the bundled version, see Rel.

Definitions #

theorem IsRefl.reflexive {α : Type u_1} {r : ααProp} [IsRefl α r] :
theorem Reflexive.rel_of_ne_imp {α : Type u_1} {r : ααProp} (h : Reflexive r) {x : α} {y : α} (hr : x yr x y) :
r x y

To show a reflexive relation r : α → α → Prop holds over x y : α, it suffices to show it holds when x ≠ y.

theorem Reflexive.ne_imp_iff {α : Type u_1} {r : ααProp} (h : Reflexive r) {x : α} {y : α} :
x yr x y r x y

If a reflexive relation r : α → α → Prop holds over x y : α, then it holds whether or not x ≠ y.

theorem reflexive_ne_imp_iff {α : Type u_1} {r : ααProp} [IsRefl α r] {x : α} {y : α} :
x yr x y r x y

If a reflexive relation r : α → α → Prop holds over x y : α, then it holds whether or not x ≠ y. Unlike Reflexive.ne_imp_iff, this uses [IsRefl α r].

theorem Symmetric.iff {α : Type u_1} {r : ααProp} (H : Symmetric r) (x : α) (y : α) :
r x y r y x
theorem Symmetric.flip_eq {α : Type u_1} {r : ααProp} (h : Symmetric r) :
flip r = r
theorem Symmetric.swap_eq {α : Type u_1} {r : ααProp} :
theorem flip_eq_iff {α : Type u_1} {r : ααProp} :
theorem swap_eq_iff {α : Type u_1} {r : ααProp} :
theorem Reflexive.comap {α : Type u_1} {β : Type u_2} {r : ββProp} (h : Reflexive r) (f : αβ) :
theorem Symmetric.comap {α : Type u_1} {β : Type u_2} {r : ββProp} (h : Symmetric r) (f : αβ) :
theorem Transitive.comap {α : Type u_1} {β : Type u_2} {r : ββProp} (h : Transitive r) (f : αβ) :
theorem Equivalence.comap {α : Type u_1} {β : Type u_2} {r : ββProp} (h : Equivalence r) (f : αβ) :
def Relation.Comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (r : αβProp) (p : βγProp) (a : α) (c : γ) :

The composition of two relations, yielding a new relation. The result relates a term of α and a term of γ if there is an intermediate term of β related to both.

Equations
Instances For
    theorem Relation.comp_eq {α : Type u_1} {β : Type u_2} {r : αβProp} :
    (Relation.Comp r fun (x1 x2 : β) => x1 = x2) = r
    theorem Relation.eq_comp {α : Type u_1} {β : Type u_2} {r : αβProp} :
    Relation.Comp (fun (x1 x2 : α) => x1 = x2) r = r
    theorem Relation.iff_comp {α : Type u_1} {r : PropαProp} :
    Relation.Comp (fun (x1 x2 : Prop) => x1 x2) r = r
    theorem Relation.comp_iff {α : Type u_1} {r : αPropProp} :
    (Relation.Comp r fun (x1 x2 : Prop) => x1 x2) = r
    theorem Relation.comp_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : αβProp} {p : βγProp} {q : γδProp} :
    theorem Relation.flip_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : αβProp} {p : βγProp} :
    def Relation.Fibration {α : Type u_1} {β : Type u_2} (rα : ααProp) (rβ : ββProp) (f : αβ) :

    A function f : α → β is a fibration between the relation and if for all a : α and b : β, whenever b : β and f a are related by , b is the image of some a' : α under f, and a' and a are related by .

    Equations
    Instances For
      theorem Acc.of_fibration {α : Type u_1} {β : Type u_2} {rα : ααProp} {rβ : ββProp} (f : αβ) (fib : Relation.Fibration f) {a : α} (ha : Acc a) :
      Acc (f a)

      If f : α → β is a fibration between relations and , and a : α is accessible under , then f a is accessible under .

      theorem Acc.of_downward_closed {α : Type u_1} {β : Type u_2} {rβ : ββProp} (f : αβ) (dc : ∀ {a : α} {b : β}, b (f a)∃ (c : α), f c = b) (a : α) (ha : Acc (InvImage f) a) :
      Acc (f a)
      def Relation.Map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (r : αβProp) (f : αγ) (g : βδ) :
      γδProp

      The map of a relation r through a pair of functions pushes the relation to the codomains of the functions. The resulting relation is defined by having pairs of terms related if they have preimages related by r.

      Equations
      Instances For
        theorem Relation.map_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : αβProp} {f : αγ} {g : βδ} {c : γ} {d : δ} :
        Relation.Map r f g c d ∃ (a : α), ∃ (b : β), r a b f a = c g b = d
        @[simp]
        theorem Relation.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} {ζ : Type u_6} (r : αβProp) (f₁ : αγ) (g₁ : βδ) (f₂ : γε) (g₂ : δζ) :
        Relation.Map (Relation.Map r f₁ g₁) f₂ g₂ = Relation.Map r (f₂ f₁) (g₂ g₁)
        @[simp]
        theorem Relation.map_apply_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : αγ} {g : βδ} (hf : Function.Injective f) (hg : Function.Injective g) (r : αβProp) (a : α) (b : β) :
        Relation.Map r f g (f a) (g b) r a b
        @[simp]
        theorem Relation.map_id_id {α : Type u_1} {β : Type u_2} (r : αβProp) :
        Relation.Map r id id = r
        instance Relation.instDecidableMapOfExistsAndEq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : αβProp} {f : αγ} {g : βδ} {c : γ} {d : δ} [Decidable (∃ (a : α), ∃ (b : β), r a b f a = c g b = d)] :
        Equations
        • Relation.instDecidableMapOfExistsAndEq = inst
        theorem Relation.ReflTransGen.cases_tail_iff {α : Type u_1} (r : ααProp) (a : α) :
        ∀ (a_1 : α), Relation.ReflTransGen r a a_1 a_1 = a ∃ (b : α), Relation.ReflTransGen r a b r b a_1
        inductive Relation.ReflTransGen {α : Type u_1} (r : ααProp) (a : α) :
        αProp

        ReflTransGen r: reflexive transitive closure of r

        Instances For
          theorem Relation.reflGen_iff {α : Type u_1} (r : ααProp) (a : α) :
          ∀ (a_1 : α), Relation.ReflGen r a a_1 a_1 = a r a a_1
          inductive Relation.ReflGen {α : Type u_1} (r : ααProp) (a : α) :
          αProp

          ReflGen r: reflexive closure of r

          Instances For
            theorem Relation.eqvGen_iff {α : Type u_1} (r : ααProp) :
            ∀ (a a_1 : α), Relation.EqvGen r a a_1 r a a_1 a_1 = a Relation.EqvGen r a_1 a ∃ (y : α), Relation.EqvGen r a y Relation.EqvGen r y a_1
            inductive Relation.EqvGen {α : Type u_1} (r : ααProp) :
            ααProp

            EqvGen r: equivalence closure of r.

            Instances For
              theorem Relation.transGen_iff {α : Sort u} (r : ααProp) :
              ∀ (a a_1 : α), Relation.TransGen r a a_1 r a a_1 ∃ (b : α), Relation.TransGen r a b r b a_1
              theorem Relation.ReflGen.to_reflTransGen {α : Type u_1} {r : ααProp} {a : α} {b : α} :
              theorem Relation.ReflGen.mono {α : Type u_1} {r : ααProp} {p : ααProp} (hp : ∀ (a b : α), r a bp a b) {a : α} {b : α} :
              instance Relation.ReflGen.instIsRefl {α : Type u_1} {r : ααProp} :
              Equations
              • =
              theorem Relation.ReflTransGen.trans {α : Type u_1} {r : ααProp} {a : α} {b : α} {c : α} (hab : Relation.ReflTransGen r a b) (hbc : Relation.ReflTransGen r b c) :
              theorem Relation.ReflTransGen.single {α : Type u_1} {r : ααProp} {a : α} {b : α} (hab : r a b) :
              theorem Relation.ReflTransGen.head {α : Type u_1} {r : ααProp} {a : α} {b : α} {c : α} (hab : r a b) (hbc : Relation.ReflTransGen r b c) :
              theorem Relation.ReflTransGen.symmetric {α : Type u_1} {r : ααProp} (h : Symmetric r) :
              theorem Relation.ReflTransGen.cases_tail {α : Type u_1} {r : ααProp} {a : α} {b : α} :
              Relation.ReflTransGen r a bb = a ∃ (c : α), Relation.ReflTransGen r a c r c b
              theorem Relation.ReflTransGen.head_induction_on {α : Type u_1} {r : ααProp} {b : α} {P : (a : α) → Relation.ReflTransGen r a bProp} {a : α} (h : Relation.ReflTransGen r a b) (refl : P b ) (head : ∀ {a c : α} (h' : r a c) (h : Relation.ReflTransGen r c b), P c hP a ) :
              P a h
              theorem Relation.ReflTransGen.trans_induction_on {α : Type u_1} {r : ααProp} {P : {a b : α} → Relation.ReflTransGen r a bProp} {a : α} {b : α} (h : Relation.ReflTransGen r a b) (ih₁ : ∀ (a : α), P ) (ih₂ : ∀ {a b : α} (h : r a b), P ) (ih₃ : ∀ {a b c : α} (h₁ : Relation.ReflTransGen r a b) (h₂ : Relation.ReflTransGen r b c), P h₁P h₂P ) :
              P h
              theorem Relation.ReflTransGen.cases_head {α : Type u_1} {r : ααProp} {a : α} {b : α} (h : Relation.ReflTransGen r a b) :
              a = b ∃ (c : α), r a c Relation.ReflTransGen r c b
              theorem Relation.ReflTransGen.cases_head_iff {α : Type u_1} {r : ααProp} {a : α} {b : α} :
              Relation.ReflTransGen r a b a = b ∃ (c : α), r a c Relation.ReflTransGen r c b
              theorem Relation.ReflTransGen.total_of_right_unique {α : Type u_1} {r : ααProp} {a : α} {b : α} {c : α} (U : Relator.RightUnique r) (ab : Relation.ReflTransGen r a b) (ac : Relation.ReflTransGen r a c) :
              theorem Relation.TransGen.to_reflTransGen {α : Type u_1} {r : ααProp} {a : α} {b : α} (h : Relation.TransGen r a b) :
              theorem Relation.TransGen.trans_left {α : Type u_1} {r : ααProp} {a : α} {b : α} {c : α} (hab : Relation.TransGen r a b) (hbc : Relation.ReflTransGen r b c) :
              Equations
              • Relation.TransGen.instTransReflTransGen = { trans := }
              Equations
              • Relation.TransGen.instTrans_mathlib = { trans := }
              theorem Relation.TransGen.head' {α : Type u_1} {r : ααProp} {a : α} {b : α} {c : α} (hab : r a b) (hbc : Relation.ReflTransGen r b c) :
              theorem Relation.TransGen.tail' {α : Type u_1} {r : ααProp} {a : α} {b : α} {c : α} (hab : Relation.ReflTransGen r a b) (hbc : r b c) :
              theorem Relation.TransGen.head {α : Type u_1} {r : ααProp} {a : α} {b : α} {c : α} (hab : r a b) (hbc : Relation.TransGen r b c) :
              theorem Relation.TransGen.head_induction_on {α : Type u_1} {r : ααProp} {b : α} {P : (a : α) → Relation.TransGen r a bProp} {a : α} (h : Relation.TransGen r a b) (base : ∀ {a : α} (h : r a b), P a ) (ih : ∀ {a c : α} (h' : r a c) (h : Relation.TransGen r c b), P c hP a ) :
              P a h
              theorem Relation.TransGen.trans_induction_on {α : Type u_1} {r : ααProp} {P : {a b : α} → Relation.TransGen r a bProp} {a : α} {b : α} (h : Relation.TransGen r a b) (base : ∀ {a b : α} (h : r a b), P ) (ih : ∀ {a b c : α} (h₁ : Relation.TransGen r a b) (h₂ : Relation.TransGen r b c), P h₁P h₂P ) :
              P h
              theorem Relation.TransGen.trans_right {α : Type u_1} {r : ααProp} {a : α} {b : α} {c : α} (hab : Relation.ReflTransGen r a b) (hbc : Relation.TransGen r b c) :
              Equations
              • Relation.TransGen.instTransReflTransGen_1 = { trans := }
              theorem Relation.TransGen.tail'_iff {α : Type u_1} {r : ααProp} {a : α} {c : α} :
              Relation.TransGen r a c ∃ (b : α), Relation.ReflTransGen r a b r b c
              theorem Relation.TransGen.head'_iff {α : Type u_1} {r : ααProp} {a : α} {c : α} :
              Relation.TransGen r a c ∃ (b : α), r a b Relation.ReflTransGen r b c
              theorem Relation.reflGen_eq_self {α : Type u_1} {r : ααProp} (hr : Reflexive r) :
              theorem Relation.reflexive_reflGen {α : Type u_1} {r : ααProp} :
              theorem Relation.reflGen_minimal {α : Type u_1} {r : ααProp} {r' : ααProp} (hr' : Reflexive r') (h : ∀ (x y : α), r x yr' x y) {x : α} {y : α} (hxy : Relation.ReflGen r x y) :
              r' x y
              theorem Relation.transGen_eq_self {α : Type u_1} {r : ααProp} (trans : Transitive r) :
              theorem Relation.transitive_transGen {α : Type u_1} {r : ααProp} :
              instance Relation.instIsTransTransGen {α : Type u_1} {r : ααProp} :
              Equations
              • =
              theorem Relation.TransGen.lift {α : Type u_1} {β : Type u_2} {r : ααProp} {p : ββProp} {a : α} {b : α} (f : αβ) (h : ∀ (a b : α), r a bp (f a) (f b)) (hab : Relation.TransGen r a b) :
              Relation.TransGen p (f a) (f b)
              theorem Relation.TransGen.lift' {α : Type u_1} {β : Type u_2} {r : ααProp} {p : ββProp} {a : α} {b : α} (f : αβ) (h : ∀ (a b : α), r a bRelation.TransGen p (f a) (f b)) (hab : Relation.TransGen r a b) :
              Relation.TransGen p (f a) (f b)
              theorem Relation.TransGen.closed {α : Type u_1} {r : ααProp} {a : α} {b : α} {p : ααProp} :
              (∀ (a b : α), r a bRelation.TransGen p a b)Relation.TransGen r a bRelation.TransGen p a b
              theorem Relation.TransGen.closed' {α : Type u_1} {r : ααProp} {P : αProp} (dc : ∀ {a b : α}, r a bP bP a) {a : α} {b : α} (h : Relation.TransGen r a b) :
              P bP a
              theorem Relation.TransGen.mono {α : Type u_1} {r : ααProp} {a : α} {b : α} {p : ααProp} :
              (∀ (a b : α), r a bp a b)Relation.TransGen r a bRelation.TransGen p a b
              theorem Relation.transGen_minimal {α : Type u_1} {r : ααProp} {r' : ααProp} (hr' : Transitive r') (h : ∀ (x y : α), r x yr' x y) {x : α} {y : α} (hxy : Relation.TransGen r x y) :
              r' x y
              theorem Relation.TransGen.swap {α : Type u_1} {r : ααProp} {a : α} {b : α} (h : Relation.TransGen r b a) :
              theorem Relation.transGen_swap {α : Type u_1} {r : ααProp} {a : α} {b : α} :
              theorem Relation.reflTransGen_iff_eq {α : Type u_1} {r : ααProp} {a : α} {b : α} (h : ∀ (b : α), ¬r a b) :
              theorem Relation.reflTransGen_iff_eq_or_transGen {α : Type u_1} {r : ααProp} {a : α} {b : α} :
              theorem Relation.ReflTransGen.lift {α : Type u_1} {β : Type u_2} {r : ααProp} {p : ββProp} {a : α} {b : α} (f : αβ) (h : ∀ (a b : α), r a bp (f a) (f b)) (hab : Relation.ReflTransGen r a b) :
              Relation.ReflTransGen p (f a) (f b)
              theorem Relation.ReflTransGen.mono {α : Type u_1} {r : ααProp} {a : α} {b : α} {p : ααProp} :
              (∀ (a b : α), r a bp a b)Relation.ReflTransGen r a bRelation.ReflTransGen p a b
              theorem Relation.reflTransGen_eq_self {α : Type u_1} {r : ααProp} (refl : Reflexive r) (trans : Transitive r) :
              theorem Relation.reflTransGen_minimal {α : Type u_1} {r : ααProp} {r' : ααProp} (hr₁ : Reflexive r') (hr₂ : Transitive r') (h : ∀ (x y : α), r x yr' x y) {x : α} {y : α} (hxy : Relation.ReflTransGen r x y) :
              r' x y
              instance Relation.instIsReflReflTransGen {α : Type u_1} {r : ααProp} :
              Equations
              • =
              instance Relation.instIsTransReflTransGen {α : Type u_1} {r : ααProp} :
              Equations
              • =
              theorem Relation.ReflTransGen.lift' {α : Type u_1} {β : Type u_2} {r : ααProp} {p : ββProp} {a : α} {b : α} (f : αβ) (h : ∀ (a b : α), r a bRelation.ReflTransGen p (f a) (f b)) (hab : Relation.ReflTransGen r a b) :
              Relation.ReflTransGen p (f a) (f b)
              theorem Relation.reflTransGen_closed {α : Type u_1} {r : ααProp} {a : α} {b : α} {p : ααProp} :
              (∀ (a b : α), r a bRelation.ReflTransGen p a b)Relation.ReflTransGen r a bRelation.ReflTransGen p a b
              theorem Relation.ReflTransGen.swap {α : Type u_1} {r : ααProp} {a : α} {b : α} (h : Relation.ReflTransGen r b a) :
              theorem Relation.reflTransGen_swap {α : Type u_1} {r : ααProp} {a : α} {b : α} :
              theorem Relation.EqvGen.is_equivalence {α : Type u_1} (r : ααProp) :
              def Relation.EqvGen.setoid {α : Type u_1} (r : ααProp) :

              EqvGen.setoid r is the setoid generated by a relation r.

              The motivation for this definition is that Quot r behaves like Quotient (EqvGen.setoid r), see for example Quot.eqvGen_exact and Quot.eqvGen_sound.

              Equations
              Instances For
                theorem Relation.EqvGen.mono {α : Type u_1} {a : α} {b : α} {r : ααProp} {p : ααProp} (hrp : ∀ (a b : α), r a bp a b) (h : Relation.EqvGen r a b) :
                @[deprecated Relation.EqvGen.is_equivalence]
                theorem EqvGen.is_equivalence {α : Type u_1} (r : ααProp) :

                Alias of Relation.EqvGen.is_equivalence.

                @[deprecated Relation.EqvGen.setoid]
                def EqvGen.Setoid {α : Type u_1} (r : ααProp) :

                Alias of Relation.EqvGen.setoid.


                EqvGen.setoid r is the setoid generated by a relation r.

                The motivation for this definition is that Quot r behaves like Quotient (EqvGen.setoid r), see for example Quot.eqvGen_exact and Quot.eqvGen_sound.

                Equations
                Instances For
                  @[deprecated Relation.EqvGen.mono]
                  theorem EqvGen.mono {α : Type u_1} {a : α} {b : α} {r : ααProp} {p : ααProp} (hrp : ∀ (a b : α), r a bp a b) (h : Relation.EqvGen r a b) :

                  Alias of Relation.EqvGen.mono.

                  def Relation.Join {α : Type u_1} (r : ααProp) :
                  ααProp

                  The join of a relation on a single type is a new relation for which pairs of terms are related if there is a third term they are both related to. For example, if r is a relation representing rewrites in a term rewriting system, then confluence is the property that if a rewrites to both b and c, then join r relates b and c (see Relation.church_rosser).

                  Equations
                  Instances For
                    theorem Relation.church_rosser {α : Type u_1} {r : ααProp} {a : α} {b : α} {c : α} (h : ∀ (a b c : α), r a br a c∃ (d : α), Relation.ReflGen r b d Relation.ReflTransGen r c d) (hab : Relation.ReflTransGen r a b) (hac : Relation.ReflTransGen r a c) :

                    A sufficient condition for the Church-Rosser property.

                    theorem Relation.join_of_single {α : Type u_1} {r : ααProp} {a : α} {b : α} (h : Reflexive r) (hab : r a b) :
                    theorem Relation.symmetric_join {α : Type u_1} {r : ααProp} :
                    theorem Relation.reflexive_join {α : Type u_1} {r : ααProp} (h : Reflexive r) :
                    theorem Relation.transitive_join {α : Type u_1} {r : ααProp} (ht : Transitive r) (h : ∀ (a b c : α), r a br a cRelation.Join r b c) :
                    theorem Relation.equivalence_join {α : Type u_1} {r : ααProp} (hr : Reflexive r) (ht : Transitive r) (h : ∀ (a b c : α), r a br a cRelation.Join r b c) :
                    theorem Relation.equivalence_join_reflTransGen {α : Type u_1} {r : ααProp} (h : ∀ (a b c : α), r a br a c∃ (d : α), Relation.ReflGen r b d Relation.ReflTransGen r c d) :
                    theorem Relation.join_of_equivalence {α : Type u_1} {r : ααProp} {a : α} {b : α} {r' : ααProp} (hr : Equivalence r) (h : ∀ (a b : α), r' a br a b) :
                    Relation.Join r' a br a b
                    theorem Relation.reflTransGen_of_transitive_reflexive {α : Type u_1} {r : ααProp} {a : α} {b : α} {r' : ααProp} (hr : Reflexive r) (ht : Transitive r) (h : ∀ (a b : α), r' a br a b) (h' : Relation.ReflTransGen r' a b) :
                    r a b
                    theorem Relation.reflTransGen_of_equivalence {α : Type u_1} {r : ααProp} {a : α} {b : α} {r' : ααProp} (hr : Equivalence r) :
                    (∀ (a b : α), r' a br a b)Relation.ReflTransGen r' a br a b
                    theorem Quot.eqvGen_exact {α : Type u_1} {r : ααProp} {a : α} {b : α} (H : Quot.mk r a = Quot.mk r b) :
                    theorem Quot.eqvGen_sound {α : Type u_1} {r : ααProp} {a : α} {b : α} (H : Relation.EqvGen r a b) :
                    Quot.mk r a = Quot.mk r b
                    instance Quotient.decidableEq {α : Sort u_7} {s : Setoid α} [d : (a b : α) → Decidable (a b)] :
                    Equations
                    theorem Equivalence.eqvGen_iff {α : Type u_1} {r : ααProp} {a : α} {b : α} (h : Equivalence r) :
                    Relation.EqvGen r a b r a b
                    theorem Equivalence.eqvGen_eq {α : Type u_1} {r : ααProp} (h : Equivalence r) :
                    @[deprecated Quot.eqvGen_exact]
                    theorem Quot.exact {α : Type u_1} {r : ααProp} {a : α} {b : α} (H : Quot.mk r a = Quot.mk r b) :

                    Alias of Quot.eqvGen_exact.

                    @[deprecated Quot.eqvGen_sound]
                    theorem Quot.EqvGen_sound {α : Type u_1} {r : ααProp} {a : α} {b : α} (H : Relation.EqvGen r a b) :
                    Quot.mk r a = Quot.mk r b

                    Alias of Quot.eqvGen_sound.