reflTransGen_of_pred_of_le
theorem reflTransGen_of_pred_of_le :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] [inst_2 : IsPredArchimedean α] (r : α → α → Prop)
{n m : α}, (∀ i ∈ Set.Ioc n m, r (Order.pred i) i) → n ≤ m → Relation.ReflTransGen r n m
The theorem `reflTransGen_of_pred_of_le` states that for any partial ordered type `α` with a predecessor order and a property called `IsPredArchimedean`, and any relation `r` on `α`, if `n` and `m` are elements of `α` such that `n` is less than or equal to `m`, then the interval `(n, m)` is included in the reflexive-transitive closure of the relation `r` if the predecessor of every element `i` in the interval `(n, m)` is related to `i` via the relation `r`. The reflexive-transitive closure of a relation is the smallest relation that includes the original relation and is both reflexive (every element is related to itself) and transitive (if `a` is related to `b` and `b` is related to `c`, then `a` is related to `c`).
More concisely: If `α` is a partially ordered type with a predecessor order and `IsPredArchimedean` property, and `r` is a relation on `α` such that for all `i` in the interval `(n, m)` with `n ≤ m`, the predecessor of `i` is related to `i` via `r`, then the interval `(n, m)` is included in the reflexive-transitive closure of `r`.
|
transGen_of_pred_of_reflexive
theorem transGen_of_pred_of_reflexive :
∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] [inst_2 : IsPredArchimedean α] (r : α → α → Prop)
{n m : α},
Reflexive r →
(∀ i ∈ Set.Ioc m n, r i (Order.pred i)) → (∀ i ∈ Set.Ioc n m, r (Order.pred i) i) → Relation.TransGen r n m
The theorem `transGen_of_pred_of_reflexive` states that for any type `α` equipped with a linear order and a predecessor order, and for any reflexive relation `r` on `α`, if for every `i` in the interval between `m` and `n` (exclusive of `m`, inclusive of `n`), `i` is related to its predecessor, and for every `i` in the interval between `n` and `m` (exclusive of `n`, inclusive of `m`), the predecessor of `i` is related to `i`, then `(n, m)` is in the transitive closure of the relation `r`. Here, the transitive closure of a relation is the smallest transitive relation that includes the original relation, and a relation is reflexive if every element is related to itself. The predecessor of an element is defined as the largest element that is less than the given element, unless the given element is minimal, in which case its predecessor is defined to be the element itself.
More concisely: If a linear order on a type `α` has a reflexive relation `r` such that for all `i` between the elements `m` and `n`, `i` is related to its predecessor and the predecessor of `i` is related to `i`, then `(n, m)` is in the transitive closure of `r`.
|
transGen_of_pred_of_gt
theorem transGen_of_pred_of_gt :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] [inst_2 : IsPredArchimedean α] (r : α → α → Prop)
{n m : α}, (∀ i ∈ Set.Ioc m n, r i (Order.pred i)) → m < n → Relation.TransGen r n m
The theorem `transGen_of_pred_of_gt` states that for any partially ordered type `α` with a predecessor order, and a given relation `r` on `α`, if `m` is less than `n`, then the ordered pair `(n, m)` is part of the transitive closure of the relation `r` when `n` is not equal to `m`, given that `r` relates every element `i` to its predecessor within the left-open right-closed interval from `m` to `n`. In other words, if every element between `m` and `n` (excluding `m` and including `n`) is related to its predecessor via `r`, then we have a chain of connections via `r` from `n` to `m`.
More concisely: If `α` is a partially ordered type with a predecessor order, and `r` is a relation on `α` such that `m < n` implies `(n, m) ∈ r.trans` whenever every element between `m` and `n` (excluding `m` and including `n`) is related to its predecessor via `r`, then `r` is transitive.
|
reflTransGen_of_succ
theorem reflTransGen_of_succ :
∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : IsSuccArchimedean α] (r : α → α → Prop)
{n m : α},
(∀ i ∈ Set.Ico n m, r i (Order.succ i)) → (∀ i ∈ Set.Ico m n, r (Order.succ i) i) → Relation.ReflTransGen r n m
The theorem `reflTransGen_of_succ` states that for any linear order (α, ≤) endowed with a successor operation and an Archimedean property, and for any relation `r` on α, an element pair `(n, m)` belongs to the reflexive-transitive closure of `r` if the following conditions hold:
1. For all elements `i` in the left-closed right-open interval from `n` to `m` (`n ≤ i < m`), `i` is related to its successor in `r`. That is, `r i (succ i)` holds.
2. For all elements `i` in the left-closed right-open interval from `m` to `n` (`m ≤ i < n`), the successor of `i` is related to `i` in `r`. That is, `r (succ i) i` holds.
Here, the successor of an element is the least element greater than it unless it is a maximal element, in which case, the successor is the element itself. The succ-Archimedean property guarantees that for every two elements in the order, there exists a third element between them.
More concisely: For a linear order endowed with a successor operation and the Archimedean property, if for any relation `r` on the order, an element pair `(n, m)` satisfies that for all `i` in the intervals `[n, m)` and `(m, n)`, `r (i, succ i)` and `r (succ i, i)` hold respectively, then `(n, m)` is in the reflexive-transitive closure of `r`.
|
transGen_of_succ_of_reflexive
theorem transGen_of_succ_of_reflexive :
∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : IsSuccArchimedean α] (r : α → α → Prop)
{n m : α},
Reflexive r →
(∀ i ∈ Set.Ico n m, r i (Order.succ i)) → (∀ i ∈ Set.Ico m n, r (Order.succ i) i) → Relation.TransGen r n m
This theorem states that for any type `α` that is a linear order and has a successor operation, and any reflexive relation `r` on `α`, if for all elements `i` in the left-closed right-open interval from `n` to `m`, `i` is related to its successor, and for all elements `i` in the left-closed right-open interval from `m` to `n`, the successor of `i` is related to `i`, then `(n, m)` is in the transitive closure of the relation `r`. The transitive closure of a relation is the smallest relation that contains the original and is transitive. In simpler terms, `n` is related to `m` under `r` either directly or through a chain of intermediate related elements.
More concisely: If `α` is a linear order with a successor operation, `r` is a reflexive relation on `α`, and for all `i` in the interval from `n` to `m` (left-closed, right-open), `i` is related to `i'` and for all `i` in the interval from `m` to `n`, `i'` is related to `i`, then `(n, m)` is in the transitive closure of `r`.
|
reflTransGen_of_pred
theorem reflTransGen_of_pred :
∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] [inst_2 : IsPredArchimedean α] (r : α → α → Prop)
{n m : α},
(∀ i ∈ Set.Ioc m n, r i (Order.pred i)) → (∀ i ∈ Set.Ioc n m, r (Order.pred i) i) → Relation.ReflTransGen r n m
The theorem `reflTransGen_of_pred` states that, for any type `α` possessing a linear order and a predecessor order that is archimedean (meaning that for every pair of elements, there's a finite sequence of predecessor operations from the first to the second), a relation `r` holds the reflexive-transitive closure property between two elements `n` and `m`. This reflexive-transitive closure is established on the condition that for every element `i` in the left-open right-closed interval from `m` to `n`, `i` is related to its predecessor by `r`, and also for every element `i` in the left-open right-closed interval from `n` to `m`, the predecessor of `i` is related to `i` by `r`. The reflexive-transitive closure property means that `n` is related to `m` by `r` either directly or through a chain of intermediary relations within `r`.
More concisely: For any type with a linear order and an archimedean predecessor relation, the reflexive-transitive closure of a relation holds between two elements if and only if their left-open right-closed intervals contain elements related by the relation to their predecessors.
|
reflTransGen_of_succ_of_le
theorem reflTransGen_of_succ_of_le :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] [inst_2 : IsSuccArchimedean α] (r : α → α → Prop)
{n m : α}, (∀ i ∈ Set.Ico n m, r i (Order.succ i)) → n ≤ m → Relation.ReflTransGen r n m
This theorem states that for any partially ordered type `α` with a successor order that is Archimedean (i.e., there are no infinite increasing sequences), given a relation `r` and two elements `n` and `m` of type `α` such that `n ≤ m`, if for every element `i` in the left-closed right-open interval between `n` and `m`, `i` is related to its successor, then `(n, m)` is in the reflexive-transitive closure of the relation `r`. The reflexive-transitive closure of a relation is the smallest relation that contains the original relation and is both reflexive (each element is related to itself) and transitive (if `a` is related to `b` and `b` is related to `c`, then `a` is related to `c`).
More concisely: If `α` is a partially ordered type with no infinite increasing sequences, and `r` is a relation on `α` such that `n ≤ m` implies that for all `i` in the interval `(n, m)`, `i r (i' := succ i)`, then `(n, m)` is in the reflexive-transitive closure of `r`.
|
transGen_of_succ_of_lt
theorem transGen_of_succ_of_lt :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] [inst_2 : IsSuccArchimedean α] (r : α → α → Prop)
{n m : α}, (∀ i ∈ Set.Ico n m, r i (Order.succ i)) → n < m → Relation.TransGen r n m
This theorem states that for a partially ordered type `α` with a successor operation and the property that the successor of each element is greater, if `n` and `m` are two elements in `α` such that `n < m`, and a relation `r` holds between each element `i` and its successor in the left-closed right-open interval from `n` to `m`, then `(n, m)` is in the transitive closure of the relation `r`. In other words, `n` is related to `m` under the transitive closure of `r`. This means that there is a chain of elements starting at `n` and ending at `m` such that each element in the chain is related to its successor by `r`. The transitive closure of a relation `r` is the smallest relation that includes `r` and is transitive.
More concisely: If `α` is a partially ordered type with a successor operation such that the successor of each element is greater, and `n < m` in `α` with `r` holding between each `i` and its successor in the interval `[n, m)`, then `(n, m)` is in the transitive closure of `r`.
|
transGen_of_succ_of_gt
theorem transGen_of_succ_of_gt :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] [inst_2 : IsSuccArchimedean α] (r : α → α → Prop)
{n m : α}, (∀ i ∈ Set.Ico m n, r (Order.succ i) i) → m < n → Relation.TransGen r n m
The theorem `transGen_of_succ_of_gt` states that for any types `α` with a partial order and a successor order that is Archimedean, given a relation `r` and elements `n` and `m` of type `α` such that `m < n`, if for all elements `i` in the left-closed right-open interval from `m` to `n`, `r` holds between the successor of `i` and `i`, then `(n, m)` is in the transitive closure of the relation `r`. In simpler terms, if every number `i` between `m` and `n` is related to its successor under the relation `r`, then `m` is related to `n` under the transitive closure of `r`. The Archimedean property ensures that there are no infinitely small steps between `m` and `n`, so that the interval from `m` to `n` is well-behaved.
More concisely: If `α` is a type with an Archimedean partial order, `r` is a relation on `α`, `m` and `n` are elements of `α` with `m < n`, and for all `i` in the interval from `m` to `n`, `r` holds between `i` and `i'` (the successor of `i`), then `(n, m)` is in the transitive closure of `r`.
|
transGen_of_pred_of_lt
theorem transGen_of_pred_of_lt :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] [inst_2 : IsPredArchimedean α] (r : α → α → Prop)
{n m : α}, (∀ i ∈ Set.Ioc n m, r (Order.pred i) i) → n < m → Relation.TransGen r n m
This theorem states that for any partial order type `α` with a predecessor order and a property that every element has a predecessor, and for any relation `r` on `α`, if `n` and `m` are elements of `α` such that `n` is less than `m`, then the tuple `(n, m)` belongs to the transitive closure of relation `r` if and only if the predecessor of every element `i` in the interval `(n, m]` (greater than `n` and less than or equal to `m`) is related to `i` via the relation `r`. In other words, this theorem provides a condition under which an element `n` is transitively related to an element `m` in a partial order, via a relation that connects each element to its predecessor within a specific interval.
More concisely: For a partial order type with a predecessor order and the property that every element has a predecessor, an element is transitively related to another via a relation if and only if the predecessor of every element in the interval between them is related to that element via the relation.
|
transGen_of_pred_of_ne
theorem transGen_of_pred_of_ne :
∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] [inst_2 : IsPredArchimedean α] (r : α → α → Prop)
{n m : α},
(∀ i ∈ Set.Ioc m n, r i (Order.pred i)) →
(∀ i ∈ Set.Ioc n m, r (Order.pred i) i) → n ≠ m → Relation.TransGen r n m
The theorem `transGen_of_pred_of_ne` states that for any type `α` that has a linear order, predecessor order, and is pred-archimedean, and for any relation `r` on `α`, if `n` and `m` are distinct elements of `α`, then the pair `(n, m)` is in the transitive closure of the relation `r` if and only if for all elements `i` in the open-close interval from `m` to `n`, `i` is related to its predecessor, and for all elements `i` in the interval from `n` to `m`, the predecessor of `i` is related to `i`. Here, the predecessor of an element is the greatest element less than it unless the element is minimal, in which case the predecessor is the element itself.
More concisely: For any linear, pred-archimedean type `α` with a predecessor order, `(n, m)` is in the transitive closure of relation `r` if and only if for all `i` in the interval from `m` to `n`, `i` is related to its predecessor, and vice versa.
|
reflTransGen_of_pred_of_ge
theorem reflTransGen_of_pred_of_ge :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] [inst_2 : IsPredArchimedean α] (r : α → α → Prop)
{n m : α}, (∀ i ∈ Set.Ioc m n, r i (Order.pred i)) → m ≤ n → Relation.ReflTransGen r n m
This theorem states that for any type 'α' that has a partial order, a predecessor order, and whose predecessor order is Archimedean, given a relation 'r' and elements 'n' and 'm' of type 'α', if 'm' is less than or equal to 'n', then the pair '(n, m)' belongs to the reflexive-transitive closure of the relation 'r' provided that for every element 'i' in the left-open right-closed interval from 'm' to 'n', 'i' is related to its predecessor under the relation 'r'.
In simpler terms, it means that you can get from 'n' to 'm' by stepping backwards through the relation 'r', possibly without moving, as long as 'm' is not greater than 'n'.
More concisely: If 'α' is a type with a partial order, a predecessor order, and Archimedean predecessor order, then for all elements 'n' and 'm' of type 'α' with 'm' ≤ 'n', the pair '(n, m)' belongs to the reflexive-transitive closure of relation 'r' if for every 'i' in the interval from 'm' to 'n', 'i' is related to its predecessor under 'r'.
|
transGen_of_succ_of_ne
theorem transGen_of_succ_of_ne :
∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : IsSuccArchimedean α] (r : α → α → Prop)
{n m : α},
(∀ i ∈ Set.Ico n m, r i (Order.succ i)) →
(∀ i ∈ Set.Ico m n, r (Order.succ i) i) → n ≠ m → Relation.TransGen r n m
The theorem `transGen_of_succ_of_ne` states that for any types `α` with a linear order and a successor order such that the successor order is Archimedean, and for any relation `r` on `α`, if for all `i` in the left-closed right-open interval from `n` to `m`, `i` is related to its successor, and for all `i` in the left-closed right-open interval from `m` to `n`, the successor of `i` is related to `i`, then if `n` is not equal to `m`, `(n, m)` lies in the transitive closure of the relation `r`. This means that there is a sequence of related elements starting at `n` and ending at `m`. In this context, an Archimedean order is one where there are no infinite strictly increasing sequences.
More concisely: If `α` is a type with a linear and Archimedean successor order, and `r` is a relation on `α` such that for all `i` in the interval from `n` to `m` (where `n ≠ m`), `i` is related to its successor if `i` is left of `m` and the successor of `i` is related to `i` if `i` is right of `n`, then `(n, m)` is in the transitive closure of `r`.
|
reflTransGen_of_succ_of_ge
theorem reflTransGen_of_succ_of_ge :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] [inst_2 : IsSuccArchimedean α] (r : α → α → Prop)
{n m : α}, (∀ i ∈ Set.Ico m n, r (Order.succ i) i) → m ≤ n → Relation.ReflTransGen r n m
This theorem states that, for any partially ordered type `α` with a successor function that satisfies Archimedean property, and any relation `r` on `α`, if `m ≤ n` and for every `i` in the half-open interval from `m` to `n` (`m` included, `n` excluded), `r` holds between the successor of `i` and `i`, then the pair `(n, m)` lies in the reflexive-transitive closure of the relation `r`. The reflexive-transitive closure of a relation is the smallest relation that contains the original and is both reflexive and transitive. The Archimedean property in this context means there is no infinite descending chain in the order.
More concisely: If `α` is a partially ordered type with a successor function satisfying the Archimedean property, and `r` is a relation on `α` such that `r` holds between `i` and `i'` for all `i` and `i'` with `m ≤ i < n`, then `(n, m)` is in the reflexive-transitive closure of `r`.
|