Reflexive.rel_of_ne_imp
theorem Reflexive.rel_of_ne_imp :
∀ {α : Type u_1} {r : α → α → Prop}, Reflexive r → ∀ {x y : α}, (x ≠ y → r x y) → r x y
This theorem states that for any type `α` and a reflexive relation `r` on `α`, for any elements `x` and `y` of `α`, if `r` holds whenever `x` is not equal to `y`, then `r` holds for `x` and `y`. In more simple terms, it's saying that if a relation is reflexive (every element is related to itself), and it's also shown to hold when two elements are different, then it must hold for any pair of elements.
More concisely: If a reflexive relation holds for all pairs of distinct elements, then it is reflexive on the whole set.
|
Relation.ReflTransGen.head
theorem Relation.ReflTransGen.head :
∀ {α : Type u_1} {r : α → α → Prop} {a b c : α},
r a b → Relation.ReflTransGen r b c → Relation.ReflTransGen r a c
This theorem states that for any relation `r` on a type `α` and any three elements `a`, `b`, and `c` of type `α`, if `r a b` holds and `b` is related to `c` by the reflexive transitive closure of `r`, then `a` is also related to `c` by the reflexive transitive closure of `r`. In other words, the relation `r` and its reflexive transitive closure are transitive together: if `a` is related to `b` by `r`, and `b` is related to `c` through a series of steps each of which either does nothing (reflexivity) or applies `r` (transitivity), then `a` is related to `c` through a similar series of steps.
More concisely: If `r` is a relation on type `α`, and `a`, `b`, and `c` are elements of `α` with `r a b` and `b` related to `c` by the reflexive transitive closure of `r`, then `a` is related to `c` by the reflexive transitive closure of `r`.
|
Acc.of_fibration
theorem Acc.of_fibration :
∀ {α : Type u_1} {β : Type u_2} {rα : α → α → Prop} {rβ : β → β → Prop} (f : α → β),
Relation.Fibration rα rβ f → ∀ {a : α}, Acc rα a → Acc rβ (f a)
The theorem, `Acc.of_fibration`, states that given any types `α` and `β`, relations `rα` on `α` and `rβ` on `β`, and a function `f` from `α` to `β` that is a fibration between `rα` and `rβ`, then if an element `a` in `α` is accessible under the relation `rα`, the image of `a` under `f`, which is an element in `β`, is accessible under the relation `rβ`. Here, a function `f` is a fibration between `rα` and `rβ` if whenever an element `b` in `β` and the image of an element `a` in `α` under `f` are related by `rβ`, there exists an element `a'` in `α` such that `a'` and `a` are related by `rα` and `b` is the image of `a'` under `f`. An element is said to be accessible under a relation if it is not related to any infinite chain of elements under that relation.
More concisely: If `f: α → β` is a fibration between relations `rα` on `α` and `rβ` on `β`, and `a` in `α` is accessible under `rα`, then the image `f(a)` in `β` is accessible under `rβ`.
|
Relation.TransGen.head'_iff
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
This theorem asserts that for any type `α` and a binary relation `r` on `α`, the transitive closure of `r` from `a` to `c` (denoted `Relation.TransGen r a c`) is equivalent to the existence of an intermediate element `b` such that `r a b` and the reflexive transitive closure of `r` from `b` to `c` (denoted `Relation.ReflTransGen r b c`). In other words, if there is a transitive relationship from `a` to `c`, there exists some `b` such that `a` is directly related to `b`, and `b` is either equal to `c` or leads to `c` through a series of steps via `r`.
More concisely: For any type `α` and binary relation `r` on `α`, the transitive closure of `r` from `a` to `c` equals the existence of an intermediate element `b` such that `r a b` and `r`'s reflexive transitive closure from `b` to `c` holds.
|
Relation.TransGen.tail'
theorem Relation.TransGen.tail' :
∀ {α : Type u_1} {r : α → α → Prop} {a b c : α}, Relation.ReflTransGen r a b → r b c → Relation.TransGen r a c := by
sorry
This theorem states that for any type `α` and a relation `r` of type `α → α → Prop`, if there exists a reflexive and transitive closure of `r` from `a` to `b` and the relation `r` holds between `b` and `c`, then there is a transitive closure of `r` between `a` and `c`. In mathematical terms, if `a` is related to `b` via possibly multiple steps and `b` is directly related to `c`, then `a` is transitively related to `c`.
More concisely: If `r` is a reflexive and transitive relation on type `α`, and there exists a path of `r` steps from `a` to `b` and a direct `r` relation from `b` to `c`, then there is a path of `r` steps from `a` to `c`.
|
reflexive_ne_imp_iff
theorem reflexive_ne_imp_iff :
∀ {α : Type u_1} {r : α → α → Prop} [inst : IsRefl α r] {x y : α}, x ≠ y → r x y ↔ r x y
This theorem states that for any reflexive relation `r` on a type `α`, if `r` holds between two elements `x` and `y` of type `α`, then `r` will still hold even if `x` and `y` are not equal. The theorem is based on the assumption that `r` is a reflexive relation. In other words, the inequality of `x` and `y` does not affect the truth of the relation `r` between them.
More concisely: For any reflexive relation `r` on type `α`, if `x` and `y` are elements of `α` such that `r x x` holds, then `r x y` also holds.
|
Symmetric.flip_eq
theorem Symmetric.flip_eq : ∀ {α : Type u_1} {r : α → α → Prop}, Symmetric r → flip r = r
This theorem states that for any type `α` and a relation `r` on `α` that is symmetric, the flipped version of the relation (i.e., the relation obtained by reversing the order of arguments) is the same as the original relation. In mathematical terms, if `r` is a symmetric relation on `α` (that is, for all `x` and `y` in `α`, `r(x, y)` implies `r(y, x)`), then `r(x, y)` is equivalent to `r(y, x)` for all `x` and `y` in `α`, which means the relation remains the same even when the arguments are flipped.
More concisely: For any symmetric relation `r` on type `α`, `r(x, y)` is equivalent to `r(y, x)` for all `x` and `y` in `α`.
|
Relation.reflTransGen_eq_self
theorem Relation.reflTransGen_eq_self :
∀ {α : Type u_1} {r : α → α → Prop}, Reflexive r → Transitive r → Relation.ReflTransGen r = r
This theorem states that for any type `α` and any binary relation `r` on `α`, if `r` is both reflexive (i.e., every element in `α` is related to itself under `r`) and transitive (i.e., if `x` is related to `y` and `y` is related to `z`, then `x` is also related to `z` under `r`), then the reflexive and transitive closure of `r` is equal to `r` itself. In other words, if a relation is already reflexive and transitive, applying the reflexive-transitive closure operation to it doesn't change the relation.
More concisely: If a binary relation on a type is both reflexive and transitive, then its reflexive-transitive closure is equal to the relation itself.
|
Relation.transGen_reflGen
theorem Relation.transGen_reflGen :
∀ {α : Type u_1} {r : α → α → Prop}, Relation.TransGen (Relation.ReflGen r) = Relation.ReflTransGen r
This theorem states that for any type `α` and any binary relation `r` over `α`, the transitive closure of the reflexive closure of `r` is equal to the reflexive transitive closure of `r`. In mathematics, these are concepts related to how you can extend a relation - the reflexive closure adds all self-loops, the transitive closure links any two related items, while the reflexive transitive closure does both.
More concisely: The reflexive closure and transitive closure of a binary relation are equal.
|
Relation.TransGen.lift
theorem Relation.TransGen.lift :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {p : β → β → Prop} {a b : α} (f : α → β),
(∀ (a b : α), r a b → p (f a) (f b)) → Relation.TransGen r a b → Relation.TransGen p (f a) (f b)
This theorem, named `Relation.TransGen.lift`, is a statement about the transitive closure of relations in the context of type theory. Given two types `α` and `β`, two relations `r` on `α` and `p` on `β`, and a function `f` from `α` to `β`, if for every pair of elements `a` and `b` from `α` the relation `r` implies the relation `p` under the function `f`, then if `a` and `b` are related by the transitive closure of `r`, they will also be related by the transitive closure of `p` after being mapped by the function `f`. It essentially lifts a property from the relation `r` to the relation `p` under a certain function, in the context of transitive closures.
More concisely: If relation `r` on type `α` implies relation `p` on type `β` under function `f`, then the transitive closures of `r` and `p` after applying `f` are related.
|
Relation.reflGen_eq_self
theorem Relation.reflGen_eq_self : ∀ {α : Type u_1} {r : α → α → Prop}, Reflexive r → Relation.ReflGen r = r
This theorem states that for any type `α` and any binary relation `r` on `α`, if `r` is a reflexive relation (i.e., for every element `x` in `α`, `r x x` holds), then the reflexive closure of `r` (denoted by `Relation.ReflGen r`) is equal to `r` itself. In mathematical terms, if `r` is a reflexive relation on a set `α`, then the smallest reflexive relation containing `r` is `r` itself.
More concisely: If `r` is a reflexive relation on a set `α`, then `Relation.ReflGen r = r`.
|
Relation.TransGen.trans
theorem Relation.TransGen.trans :
∀ {α : Type u_1} {r : α → α → Prop} {a b c : α},
Relation.TransGen r a b → Relation.TransGen r b c → Relation.TransGen r a c
This theorem states that for any type `α` and any binary relation `r` on `α`, if there is a transitive closure of `r` from `a` to `b`, and another transitive closure of `r` from `b` to `c` (where `a`, `b`, and `c` are elements of `α`), then there is a transitive closure of `r` from `a` to `c`. In other words, the transitivity of the transitive closure of a relation is proven, i.e., if `a` is related to `b` and `b` is related to `c` via possibly multiple steps of `r`, then `a` is also related to `c` via possibly multiple steps of `r`.
More concisely: If `r` is a binary relation on type `α`, and there exist transitive closures `t1` of `r` from `a` to `b` and `t2` of `r` from `b` to `c`, then there exists a transitive closure `t` of `r` such that `a` is related to `c` via `t`.
|
Symmetric.comap
theorem Symmetric.comap :
∀ {α : Type u_1} {β : Type u_2} {r : β → β → Prop}, Symmetric r → ∀ (f : α → β), Symmetric (r on f)
The theorem `Symmetric.comap` states that for any two types `α` and `β`, and a relation `r` on `β` that is symmetric, for any function `f` from `α` to `β`, the relation `r` composed with `f` (denoted by `r on f`), is also symmetric. In other words, if `x` and `y` are any two elements of `α`, and `r` holds between `f(x)` and `f(y)`, then `r` also holds between `f(y)` and `f(x)`. This theorem extends the symmetric property of a relation to the function's image under this relation.
In mathematical terms, if `r` is a symmetric relation in the sense that whenever `r(x, y)` holds then `r(y, x)` holds, then the image of this relation under any function `f: α → β` is also symmetric.
More concisely: If `r` is a symmetric relation on `β` and `f` is a function from `α` to `β`, then the relation `r` composed with `f` (denoted `r on f`) is symmetric. That is, if `r(f(x), f(y))` holds, then `r(f(y), f(x))` holds for all `x, y` in `α`.
|
Reflexive.ne_imp_iff
theorem Reflexive.ne_imp_iff : ∀ {α : Type u_1} {r : α → α → Prop}, Reflexive r → ∀ {x y : α}, x ≠ y → r x y ↔ r x y
This theorem states that, for any type `α` and a reflexive relation `r` over `α`, given any two elements `x` and `y` of `α`, if `x` is not equal to `y`, then the statement that `r` holds between `x` and `y` is logically equivalent to the straightforward claim that `r` holds between `x` and `y`. In other words, the inequality of `x` and `y` does not affect whether the reflexive relation `r` applies to `x` and `y`. This is expected, as reflexive relations hold for every pair of identical elements by definition, and this theorem extends the hold to distinct elements as well.
More concisely: For any reflexive relation `r` on type `α`, and all `x` and `y` in `α` with `x ≠ y`, the statements `r x y` and `x ≠ y ∧ r x x ∧ r y y ∧ ∀z (r z z ↔ z = x ∨ z = y)` are logically equivalent.
|
Relation.transGen_eq_self
theorem Relation.transGen_eq_self : ∀ {α : Type u_1} {r : α → α → Prop}, Transitive r → Relation.TransGen r = r := by
sorry
The theorem `Relation.transGen_eq_self` states that for any given type `α` and a relation `r` on `α`, if the relation `r` is transitive, then the transitive closure of `r` (denoted by `Relation.TransGen r`) is equal to `r` itself. The transitive closure of a relation is the smallest relation that contains the original and is transitive. This theorem therefore says that if the original relation is already transitive, then its transitive closure doesn't add any new relations.
More concisely: If a relation on a type is transitive, then its transitive closure equals the relation itself.
|
Relation.TransGen.to_reflTransGen
theorem Relation.TransGen.to_reflTransGen :
∀ {α : Type u_1} {r : α → α → Prop} {a b : α}, Relation.TransGen r a b → Relation.ReflTransGen r a b
This theorem states that for any type `α` and for any binary relation `r` on `α`, if the transitive closure of `r` relates two elements `a` and `b` of `α`, then the reflexive transitive closure of `r` also relates `a` and `b`. In mathematical terms, this theorem is saying that if `a` is related to `b` through a series of steps where each step is defined by the relation `r`, then `a` is also related to `b` in a series of steps defined by `r` where we can also stay at the same element.
More concisely: If `r` is a binary relation on type `α` and `a` and `b` are related in the transitive closure of `r`, then `a` and `b` are also related in the reflexive transitive closure of `r`.
|
Equivalence.eqvGen_iff
theorem Equivalence.eqvGen_iff :
∀ {α : Type u_1} {r : α → α → Prop} {a b : α}, Equivalence r → (EqvGen r a b ↔ r a b)
This theorem, named `Equivalence.eqvGen_iff`, is about an equivalence relation `r` on a type `α`. Given elements `a` and `b` of this type, the theorem states that if `r` is an equivalence relation, then the `EqvGen r a b` (the reflexive, symmetric, and transitive closure of `r`) is equivalent to `r a b`. In other words, if `r` is an equivalence relation, `a` and `b` are related by the closure of `r` if and only if `a` and `b` are directly related by `r`.
More concisely: For an equivalence relation `r` on type `α` and elements `a` and `b` of `α`, `EqvGen r a b` is equivalent to `r a b`.
|
EqvGen.mono
theorem EqvGen.mono :
∀ {α : Type u_1} {a b : α} {r p : α → α → Prop}, (∀ (a b : α), r a b → p a b) → EqvGen r a b → EqvGen p a b := by
sorry
This theorem states that for any type `α` and any elements `a` and `b` of this type, given two relations `r` and `p` on `α`, if it is the case that whenever `r` holds between any two elements of `α`, `p` also holds between them, then `EqvGen r a b` implies `EqvGen p a b`. In simpler terms, `EqvGen` is a type that describes equivalence relations generated by a given relation, so the theorem is stating that if `r` is a sub-relation of `p`, then any equivalence generated by `r` is also an equivalence generated by `p`.
More concisely: If relation `r` implies relation `p` and `EqvGen` generates the equivalence relation of `r` for elements `a` and `b`, then `EqvGen` also generates the equivalence relation of `p` for `a` and `b`.
|
Symmetric.iff
theorem Symmetric.iff : ∀ {α : Type u_1} {r : α → α → Prop}, Symmetric r → ∀ (x y : α), r x y ↔ r y x
The theorem `Symmetric.iff` states that for any type `α` and a binary relation `r` on `α`, if the relation `r` is symmetric, then for all elements `x` and `y` of `α`, `r x y` is true if and only if `r y x` is true. In other words, a relation is symmetric if it holds that whenever `x` is related to `y`, `y` is also related to `x`.
More concisely: For any binary relation `r` on type `α`, `r` is symmetric if and only if for all `x` and `y` in `α`, `r x y` implies `r y x`.
|
Relation.ReflTransGen.lift
theorem Relation.ReflTransGen.lift :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {p : β → β → Prop} {a b : α} (f : α → β),
(∀ (a b : α), r a b → p (f a) (f b)) → Relation.ReflTransGen r a b → Relation.ReflTransGen p (f a) (f b)
This theorem states that for any two types `α` and `β`, relations `r` and `p` on `α` and `β` respectively, and a function `f` from `α` to `β`, if every pair `(a, b)` that satisfies the relation `r` also satisfies the relation `p` after being transformed by `f`, then `Relation.ReflTransGen r a b` implies `Relation.ReflTransGen p (f a) (f b)`. In other words, it lifts the reflexive transitive closure of a relation from one domain to another through a function, provided that the function respects the relation.
More concisely: If function `f` preserves relation `r` that is reflexively transitive on type `α`, then `Relation.ReflTrans p (f x) (f y)` holds whenever `Relation.ReflTransGen r x y` does, for types `α` and `β` and relations `r` on `α` and `p` on `β`.
|
Relation.reflTransGen_of_transitive_reflexive
theorem Relation.reflTransGen_of_transitive_reflexive :
∀ {α : Type u_1} {r : α → α → Prop} {a b : α} {r' : α → α → Prop},
Reflexive r → Transitive r → (∀ (a b : α), r' a b → r a b) → Relation.ReflTransGen r' a b → r a b
The theorem `Relation.reflTransGen_of_transitive_reflexive` states that given a type `α` and two binary relations `r` and `r'` over `α`, if `r` is reflexive and transitive, and `r'` implies `r`, then for any elements `a` and `b` of type `α`, if `a` and `b` are related by the reflexive-transitive closure of `r'` (i.e., `a` and `b` are related through a series of steps where each step is either a reflexive application or a `r'`-relation), then `a` is `r`-related to `b`. In other words, the reflexive-transitive closure of a relation `r'` that is a sub-relation of a transitive and reflexive relation `r`, is also a sub-relation of `r`.
More concisely: If `r` is a reflexive and transitive relation on type `α`, and `r' ⊆ r` is also a relation, then the reflexive-transitive closure of `r'` is a sub-relation of `r`.
|
Relation.reflexive_reflTransGen
theorem Relation.reflexive_reflTransGen : ∀ {α : Type u_1} {r : α → α → Prop}, Reflexive (Relation.ReflTransGen r) := by
sorry
This theorem states that, for any type `α` and any binary relation `r` on `α`, the reflexive-transitive closure of `r` is a reflexive relation. In other words, for any element of `α`, the element is related to itself in the reflexive-transitive closure of `r`.
The reflexive-transitive closure of a relation `r` is the smallest reflexive and transitive relation that contains `r`. So, this theorem is stating a fundamental property of reflexive-transitive closures: every element is related to itself.
More concisely: The reflexive-transitive closure of a binary relation is a reflexive relation.
|
Relation.transitive_reflTransGen
theorem Relation.transitive_reflTransGen : ∀ {α : Type u_1} {r : α → α → Prop}, Transitive (Relation.ReflTransGen r)
The theorem `Relation.transitive_reflTransGen` states that for any type `α` and for any binary relation `r` on `α`, the reflexive transitive closure of `r` is transitive. More specifically, if we have elements `x`, `y`, and `z` of type `α` such that `x` is related to `y` and `y` is related to `z` under the reflexive transitive closure of `r`, then `x` is also related to `z` under the same closure. The reflexive transitive closure of a relation is the smallest relation that contains the original one and is both reflexive (every element is related to itself) and transitive.
More concisely: If a relation is reflexive and transitive, then its reflexive transitive closure is transitive.
|
Relation.ReflTransGen.single
theorem Relation.ReflTransGen.single :
∀ {α : Type u_1} {r : α → α → Prop} {a b : α}, r a b → Relation.ReflTransGen r a b
This theorem states that, for any type `α`, relation `r` and elements `a` and `b` of type `α`, if the relation `r` holds between `a` and `b`, then `a` and `b` are in the reflexive transitive closure of the relation `r`. In other words, a single application of a relation `r` is sufficient to establish a connection in its reflexive transitive closure.
More concisely: For any relation `r` on type `α`, if `r` is reflexive and transitive, then the reflexive transitive closure of `r` is equal to `r` itself.
|
Relation.reflTransGen_iff_eq_or_transGen
theorem Relation.reflTransGen_iff_eq_or_transGen :
∀ {α : Type u_1} {r : α → α → Prop} {a b : α}, Relation.ReflTransGen r a b ↔ b = a ∨ Relation.TransGen r a b := by
sorry
This theorem states that for any type `α` and a binary relation `r` on `α`, and given two elements `a` and `b` of type `α`, the reflexive transitive closure of `r` holds between `a` and `b` if and only if `b` equals `a` or the transitive closure of `r` holds between `a` and `b`. In other words, either `a` and `b` are the same, or there is a chain of `r`-related elements starting from `a` and ending at `b`.
More concisely: The reflexive transitive closure of a binary relation `r` on type `α` holds between elements `a` and `b` if and only if `b` equals `a` or there exists a chain of `r`-related elements connecting `a` to `b`.
|
Relation.ReflTransGen.cases_head
theorem Relation.ReflTransGen.cases_head :
∀ {α : Type u_1} {r : α → α → Prop} {a b : α},
Relation.ReflTransGen r a b → a = b ∨ ∃ c, r a c ∧ Relation.ReflTransGen r c b
This theorem, `Relation.ReflTransGen.cases_head`, states that for any type `α` and any binary relation `r` on `α`, for any two elements `a` and `b` of the type, if the reflexive transitive closure (denoted by `Relation.ReflTransGen r`) of `r` relates `a` to `b`, then either `a` is equal to `b`, or there exists an element `c` such that `r` relates `a` to `c` and the reflexive transitive closure of `r` relates `c` to `b`. The reflexive transitive closure of a relation is a new relation that relates any element to itself, and if the original relation relates an element `x` to an element `y` and `y` to an element `z`, then the closure also relates `x` to `z`.
More concisely: If `Relation.ReflTransGen r` relates `a` to `b`, then there exists `c` such that `r` relates `a` to `c` and `Relation.ReflTransGen r` relates `c` to `b`, or `a = b`.
|
Relation.ReflTransGen.trans
theorem Relation.ReflTransGen.trans :
∀ {α : Type u_1} {r : α → α → Prop} {a b c : α},
Relation.ReflTransGen r a b → Relation.ReflTransGen r b c → Relation.ReflTransGen r a c
This theorem states that for any type `α`, and any relation `r` of type `α → α → Prop`, if `a`, `b`, and `c` are of type `α`, then if `Relation.ReflTransGen r a b` and `Relation.ReflTransGen r b c` hold true, so does `Relation.ReflTransGen r a c`. In simpler terms, if there is a reflexive transitive relation from `a` to `b`, and from `b` to `c`, then there is also a reflexive transitive relation from `a` to `c`. This is essentially a generalization of the transitivity property for reflexive transitive relations.
More concisely: If `r` is a reflexive and transitive relation on type `α`, then for all `a, b, c` in `α`, if `r a b` and `r b c` hold, then `r a c` holds as well.
|
Relation.TransGen.head
theorem Relation.TransGen.head :
∀ {α : Type u_1} {r : α → α → Prop} {a b c : α}, r a b → Relation.TransGen r b c → Relation.TransGen r a c := by
sorry
This theorem, "Relation.TransGen.head", states that for any set `α`, any binary relation `r` on `α`, and any three elements `a`, `b`, and `c` from `α`, if `r` holds between `a` and `b` and there exists a transitive closure of `r` between `b` and `c`, then there also exists a transitive closure of `r` between `a` and `c`. In other words, this theorem entails that if `a` is related to `b`, and `b` is in some way related to `c` through a chain of relations, then `a` is also related to `c` through a similar chain of relations.
More concisely: If `r` is a transitive relation on set `α`, and `a` is related to `b` by `r`, and there exists a chain of `r`-related elements from `b` to `c`, then `a` is related to `c` by `r`.
|
Relation.church_rosser
theorem Relation.church_rosser :
∀ {α : Type u_1} {r : α → α → Prop} {a b c : α},
(∀ (a b c : α), r a b → r a c → ∃ d, Relation.ReflGen r b d ∧ Relation.ReflTransGen r c d) →
Relation.ReflTransGen r a b → Relation.ReflTransGen r a c → Relation.Join (Relation.ReflTransGen r) b c
The theorem `Relation.church_rosser` states a sufficient condition for the Church-Rosser property in relation to a given relation `r` on a type `α`. The Church-Rosser property is characterized by the ability of two elements `b` and `c` to be related by the join of the reflexive transitive closure of `r`, given that they both are related to some common element `a` through the reflexive transitive closure of `r`. The sufficient condition to ensure this property holds is that for any three elements `a`, `b`, and `c`, if both `b` and `c` can be directly reached from `a` by the relation `r`, then there exists a common element `d` which can be reached from `b` via reflexive relation and from `c` via reflexive-transitive relation.
More concisely: If relation `r` on type `α` satisfies the property that for all `a`, `b`, `c`, if `b` and `c` are related to `a` by `r`, then there exists an element `d` reachable from `b` by the reflexive relation and from `c` by the reflexive-transitive relation, then `r` has the Church-Rosser property.
|
Relation.reflTransGen_iff_eq
theorem Relation.reflTransGen_iff_eq :
∀ {α : Type u_1} {r : α → α → Prop} {a b : α}, (∀ (b : α), ¬r a b) → (Relation.ReflTransGen r a b ↔ b = a) := by
sorry
This theorem states that for any type `α` and any binary relation `r` defined on `α`, and given any two elements `a` and `b` from `α`, if `a` does not relate to any other element `b` in `α` through `r`, then the reflexive transitive closure of `r` from `a` to `b` is equivalent to `b` being equal to `a`. In other words, if there's no way to get from `a` to any other element `b` through the relation `r`, then the only way for the reflexive transitive closure of `r` to hold between `a` and `b` is if `b` is actually the same as `a`.
More concisely: If there is no `x` such that `a` `r` `x` and `x` `r` `b` for a binary relation `r` on type `α`, then `a` and `b` are equal.
|