sbtw_cyclic
theorem sbtw_cyclic : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c ↔ sbtw c a b
This theorem, `sbtw_cyclic`, states that for any type `α` that has a `CircularPreorder` instance, and for any three elements `a`, `b`, and `c` of type `α`, the relation `sbtw a b c` (sbtw stands for "strictly between") is equivalent to the relation `sbtw c a b`. In other words, if `b` is strictly between `a` and `c` in a circular order, then `a` is strictly between `c` and `b`.
More concisely: For any type `α` with a `CircularPreorder` instance, the relation `a sbtw b c` if and only if `c sbtw b a`.
|
CircularPreorder.btw_cyclic_left
theorem CircularPreorder.btw_cyclic_left :
∀ {α : Type u_1} [self : CircularPreorder α] {a b c : α}, btw a b c → btw b c a
The theorem `CircularPreorder.btw_cyclic_left` states that for any type `α` with a `CircularPreorder` and given three elements `a`, `b`, and `c` of type `α`, if `b` is between `a` and `c`, then `c` is between `b` and `a`. This is analogous to having three points on a circle where the order of the points allows for a cyclic traversal.
More concisely: If `a` `CircularPreorder` `b` and `b` `CircularPreorder` `c` in a type `α` with a `CircularPreorder`, then `c` `CircularPreorder` `a`.
|
SBtw.sbtw.cyclic_right
theorem SBtw.sbtw.cyclic_right : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → sbtw c a b := by
sorry
This theorem, `SBtw.sbtw.cyclic_right`, states that for any circular preorder type `α` and any three elements `a`, `b`, `c` of type `α`, if `b` is strictly between `a` and `c` (`sbtw a b c`), then `a` is strictly between `c` and `b` (`sbtw c a b`). A circular preorder is a type with a binary relation that is reflexive, transitive, and cyclic (if `a ≤ b` and `b ≤ a`, then `b ≤ c` and `c ≤ a`), and `sbtw` designates strict betweenness.
More concisely: If `a`, `b`, and `c` are elements of a circular preorder type, and `b` is strictly between `a` and `c` (`sbtw a b c`), then `a` is strictly between `c` and `b` (`sbtw c a b`).
|
sbtw_iff_btw_not_btw
theorem sbtw_iff_btw_not_btw :
∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c ↔ btw a b c ∧ ¬btw c b a
This theorem states that for any type `α` that is equipped with a circular preorder, and for any three elements `a`, `b`, and `c` of this type, `a` is strictly between `b` and `c` if and only if `a` is between `b` and `c` and `c` is not between `b` and `a`. In other words, the condition for strict betweenness is that `a` is between `b` and `c`, but `c` can't be between `b` and `a`.
More concisely: For any type `α` with a circular preorder, element `a` is strictly between `b` and `c` if and only if `a` is between `b` and `c` and there is no `d` such that `b` is between `a` and `d` and `d` is between `a` and `c`.
|
CircularPreorder.btw_refl
theorem CircularPreorder.btw_refl : ∀ {α : Type u_1} [self : CircularPreorder α] (a : α), btw a a a
This theorem states that for any type `α` that has a `CircularPreorder` structure, an element `a` of type `α` is considered to be between itself and itself. In mathematical terms, this would be expressed as "for all `α` in a circular preorder, `a` is between `a` and `a`".
More concisely: In a circular preorder, every element is between itself and itself.
|
btw_cyclic
theorem btw_cyclic : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, btw a b c ↔ btw c a b
This theorem states that for any type `α` that follows a circular preorder, and for any three elements `a`, `b`, and `c` of type `α`, the relation "betweenness" (`btw`) observed from `a` to `b` to `c` is equivalent to the "betweenness" observed from `c` to `a` to `b`. The comment also mentions that the direction of the `↔` in the theorem was intentionally chosen so that using the `rw` tactic with `[btw_cyclic]` or `[← btw_cyclic]` in Lean cycles the terms to the right or left respectively.
More concisely: For any type `α` following a circular preorder and any elements `a, b, c` of type `α`, the betweenness relations `a b c` and `c a b` are equivalent.
|
SBtw.sbtw.trans_right
theorem SBtw.sbtw.trans_right :
∀ {α : Type u_1} [inst : CircularPreorder α] {a b c d : α}, sbtw a b c → sbtw a c d → sbtw a b d
This theorem, titled `sbtw.trans_right`, states that for any type `α` that has a structure of `CircularPreorder`, and for any four elements `a, b, c, d` of this type, if `a` is strictly between `b` and `c` (`sbtw a b c`), and `a` is also strictly between `c` and `d` (`sbtw a c d`), then `a` is strictly between `b` and `d` (`sbtw a b d`). This theorem is an alias of `sbtw_trans_right` and represents a transitive property in a circular preorder context.
More concisely: If `a` is strictly between `b` and `c` and strictly between `c` and `d` in a circular preorder, then `a` is strictly between `b` and `d`.
|
CircularPartialOrder.btw_antisymm
theorem CircularPartialOrder.btw_antisymm :
∀ {α : Type u_1} [self : CircularPartialOrder α] {a b c : α}, btw a b c → btw c b a → a = b ∨ b = c ∨ c = a := by
sorry
This theorem states that, for any three points `a`, `b`, and `c` in a circular partially ordered set `α`, if `b` is between `a` and `c` and `b` is also between `c` and `a`, then at least one of the following must be true: `a` is identical to `b`, `b` is identical to `c`, or `c` is identical to `a`. A circular partially ordered set is a type of set where the betweenness (`btw`) relation is not necessarily transitive, reflecting some sort of "circular" structure in the ordering of its elements.
More concisely: In a circular partially ordered set, if point `b` is between points `a` and `c`, and `b` is also between `c` and `a`, then `a`, `b`, and `c` are pairwise identical.
|
Btw.btw.cyclic_right
theorem Btw.btw.cyclic_right : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, btw a b c → btw c a b := by
sorry
This theorem, `Btw.btw.cyclic_right`, is an alias of `btw_cyclic_right`. It states that for any type `α` that has a `CircularPreorder` (a type of order where for any three elements, if the first is less than the second and the second is less than the third, then the third is also less than the first), given three elements `a`, `b`, and `c` of this type, if `a` is between `b` and `c` (`btw a b c`), then it follows that `c` is between `a` and `b` (`btw c a b`).
More concisely: If `α` is a type with a CircularPreorder and `a`, `b`, `c` are elements of `α` such that `a` is between `b` and `c` (`btw a b c`), then `c` is also between `a` and `b` (`btw c a b`).
|
SBtw.sbtw.not_sbtw
theorem SBtw.sbtw.not_sbtw : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → ¬sbtw c b a := by
sorry
This theorem, which is an alias of `sbtw_asymm`, states that for any type `α` that has a `CircularPreorder` instance and any three elements `a`, `b`, and `c` of this type, if `a` is strictly between `b` and `c` (expressed as `sbtw a b c`), then `c` is not strictly between `b` and `a` (expressed as `¬sbtw c b a`). In other words, the strict betweenness relation is asymmetric.
More concisely: If `a` strictly between `b` and `c` in a type with a `CircularPreorder` instance, then `c` is not strictly between `b` and `a`.
|
Btw.btw.cyclic_left
theorem Btw.btw.cyclic_left : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, btw a b c → btw b c a := by
sorry
This theorem, `Btw.btw.cyclic_left`, states that for any type `α` that has a circular preorder (a relation that is reflexive and transitive), and for any three elements `a`, `b`, and `c` of this type, if `a` is between `b` and `c` (denoted as `btw a b c`), then `b` is between `c` and `a` (denoted as `btw b c a`). This is essentially a property of circularity where the betweenness relation is cyclic.
More concisely: For any type with a circular preorder, if `a` is between `b` and `c`, then `b` is between `c` and `a` (i.e., the betweenness relation is reflexively cyclic).
|
Btw.btw.sbtw_of_not_btw
theorem Btw.btw.sbtw_of_not_btw :
∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, btw a b c → ¬btw c b a → sbtw a b c
This theorem, "sbtw_of_not_btw", states that for any type 'α' which has a circular preorder, given three elements 'a', 'b', and 'c' of this type, if 'b' is between 'a' and 'c' and 'b' is not between 'c' and 'a', then 'b' is strictly between 'a' and 'c'. Here, 'btw' stands for 'between' and 'sbtw' stands for 'strictly between'.
More concisely: If 'a' circularly preorders 'b' and 'b' circularly preorders 'c' but not vice versa, then 'b' strictly preorders both 'a' and 'c'.
|
CircularOrder.btw_total
theorem CircularOrder.btw_total : ∀ {α : Type u_1} [self : CircularOrder α] (a b c : α), btw a b c ∨ btw c b a := by
sorry
This theorem, named `CircularOrder.btw_total`, states that for any three points in a circular order (a specific type of ordering), the second point is always between the other two points. Specifically, either the arrangement is such that point 'a' is before point 'b' and point 'b' is before point 'c' (denoted as `btw a b c`), or point 'c' is before point 'b' and point 'b' is before point 'a' (denoted as `btw c b a`). This applies to any type `α` that has a circular order.
More concisely: For any three points `a`, `b`, and `c` in a circular order, either `b` is between `a` and `c` (`btw a b c`) or `c` is between `b` and `a` (`btw c b a`).
|
sbtw_irrefl_left_right
theorem sbtw_irrefl_left_right : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b : α}, ¬sbtw a b a
This theorem states that for any type `α`, which forms a circular preorder, and any elements `a` and `b` of this type, `a` cannot be strictly between `a` and `b`. In other words, in the context of a circular preorder, it is not possible for an element to be strictly between itself and another element.
More concisely: In a circular preorder, no element is strictly between itself and another element.
|
CircularPreorder.sbtw_iff_btw_not_btw
theorem CircularPreorder.sbtw_iff_btw_not_btw :
∀ {α : Type u_1} [self : CircularPreorder α] {a b c : α}, sbtw a b c ↔ btw a b c ∧ ¬btw c b a
The theorem `CircularPreorder.sbtw_iff_btw_not_btw` in the Lean 4 language defines strict betweenness in the context of a circular preorder. Given any three elements `a`, `b`, and `c` of a type `α` that forms a circular preorder, `b` is strictly between `a` and `c` if and only if `b` is between `a` and `c` and it is not true that `b` is between `c` and `a`.
More concisely: For all types `α` and elements `a, b, c` of `α` forming a circular preorder, `b` is strictly between `a` and `c` if and only if `b` is between `a` and `c` and not between `c` and `a`.
|
SBtw.sbtw.btw
theorem SBtw.sbtw.btw : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → btw a b c
This theorem, `SBtw.sbtw.btw`, establishes that for any type `α` following a circular preorder, if a value `b` is strictly between `a` and `c` (denoted as `sbtw a b c`), then `b` is also between `a` and `c` (denoted as `btw a b c`). In essence, it shows that strict betweenness implies betweenness in a circular preorder setting.
More concisely: In a circular preorder, if `b` strictly lies between `a` and `c` (`sbtw a b c`), then `b` also lies between `a` and `c` (`btw a b c`).
|
SBtw.sbtw.not_btw
theorem SBtw.sbtw.not_btw : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → ¬btw c b a := by
sorry
This theorem states that for any type `α` that has a CircularPreorder relation, and for any three elements `a`, `b`, and `c` of this type, if 'strictly between' (`sbtw`) relation holds for `a`, `b`, `c` (i.e., `b` is strictly between `a` and `c`), then 'between' (`btw`) relation cannot hold for `c`, `b`, `a` (i.e., `b` cannot be between `c` and `a`). In other words, if `b` is strictly between `a` and `c`, then `b` cannot be between `a` and `c` in the reverse order.
More concisely: If `β:` CircularPreorder α, `a b c:` α, and `b` is strictly between `a` and `c` (`b sbtw a c`), then `b` is not between `c` and `a` (`~b btw c a`).
|
SBtw.sbtw.cyclic_left
theorem SBtw.sbtw.cyclic_left : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → sbtw b c a := by
sorry
This is a theorem in Lean 4 which states that for any type `α` that has a circular preorder, if `a`, `b`, and `c` are instances of this type and `a` is strictly between `b` and `c` (`sbtw a b c`), then `b` is strictly between `c` and `a` (`sbtw b c a`). This theorem essentially shows the cyclic property of a circular preorder.
More concisely: In a circular preorder, if `a` is strictly between `b` and `c`, then `b` is strictly between `c` and `a`.
|
Btw.btw.not_sbtw
theorem Btw.btw.not_sbtw : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, btw a b c → ¬sbtw c b a
This theorem, `Btw.btw.not_sbtw`, states that for any circular preorder (a type of mathematical structure) of some type `α`, and any three elements `a`, `b`, and `c` of that type, if `b` is between `a` and `c` (`btw a b c`), then it is not the case that `c` is strictly between `b` and `a` (`¬sbtw c b a`). In other words, the ordering of elements in a circular preorder is such that if `b` lies between `a` and `c`, you cannot have `c` strictly lying between `b` and `a`.
More concisely: In a circular preorder, if `b` is between `a` and `c` (`btw a b c`), then `c` is not strictly between `b` and `a` (`¬sbtw c b a`).
|
CircularPreorder.sbtw_trans_left
theorem CircularPreorder.sbtw_trans_left :
∀ {α : Type u_1} [self : CircularPreorder α] {a b c d : α}, sbtw a b c → sbtw b d c → sbtw a d c
The theorem `CircularPreorder.sbtw_trans_left` states that for any type `α` equipped with a `CircularPreorder`, if we have four elements `a`, `b`, `c`, and `d` such that `b` is strictly between `a` and `c`, and `d` is strictly between `b` and `c`, then `d` is also strictly between `a` and `c`. In essence, this is capturing the transitive nature of the "strictly between" relation in a circular preorder when the value `c` is kept fixed.
More concisely: In a circular preorder on type `α`, if `b` strictly lies between `a` and `c`, and `d` strictly lies between `b` and `c`, then `d` strictly lies between `a` and `c`.
|