trans
theorem trans : ∀ {α : Sort u} {r : α → α → Prop} [inst : IsTrans α r] {a b c : α}, r a b → r b c → r a c
This theorem, "trans", states that for any type `α`, any relation `r` on `α`, and any three elements `a`, `b`, and `c` of type `α`, if `r` is transitive (as ensured by the `IsTrans` typeclass instance), then if `r a b` and `r b c` hold, then `r a c` also holds. In more traditional mathematical notation, this is saying that for all `a`, `b`, `c` in some set, if `a r b` and `b r c` then `a r c`. This is one of the defining properties of a transitive relation.
More concisely: If `r` is a transitive relation on type `α`, then `aRb` and `bRc` imply `aRc`.
|
irrefl
theorem irrefl : ∀ {α : Sort u} {r : α → α → Prop} [inst : IsIrrefl α r] (a : α), ¬r a a
This theorem, named `irrefl`, declares that for any type `α` and a relation `r` defined on `α`, if `r` is an irreflexive relation (as defined by the `IsIrrefl` typeclass), then for any element `a` of type `α`, `r a a` (i.e., `a` is related to itself by `r`) is not true. In other words, no element of an irreflexive relation is related to itself.
More concisely: For any type `α` and irreflexive relation `r` on `α`, there is no element `a` in `α` such that `r a a` holds.
|
refl
theorem refl : ∀ {α : Sort u} {r : α → α → Prop} [inst : IsRefl α r] (a : α), r a a
This theorem, named `refl`, is stating that for any type `α` (which could be of any sort `u`), given a binary relation `r` on `α` and given that `r` is reflexive on `α` (as indicated by the `IsRefl α r` instance), then for any element `a` of `α`, the relation `r` holds between `a` and itself. In other words, it's asserting the reflexive property of the relation `r`: every element is related to itself.
More concisely: For any reflexive binary relation `r` on type `α`, `r a a` holds for every `a` in `α`.
|
trans_of
theorem trans_of : ∀ {α : Sort u} (r : α → α → Prop) [inst : IsTrans α r] {a b c : α}, r a b → r b c → r a c
This theorem, called `trans_of`, states that for any type `α` and any relation `r` on `α` that is transitive (as indicated by `IsTrans α r`), if `r` holds between elements `a` and `b`, and between `b` and `c`, then `r` also holds between `a` and `c`. In other words, this is a formal statement of the transitive property: if `a` is related to `b` and `b` is related to `c`, then `a` is related to `c`.
More concisely: If `r` is a transitive relation on type `α`, then for all `a`, `b`, and `c` in `α`, if `a` is related to `b` and `b` is related to `c` (`r a b` and `r b c`), then `a` is related to `c` (`r a c`).
|
trichotomous
theorem trichotomous : ∀ {α : Sort u} {r : α → α → Prop} [inst : IsTrichotomous α r] (a b : α), r a b ∨ a = b ∨ r b a
This theorem, named `trichotomous`, states that for any type `α` and a relation `r` on `α`, if `r` is trichotomous (as defined by the typeclass `IsTrichotomous`), then for all elements `a` and `b` of type `α`, one and only one of the following holds: `r a b`, `a = b`, or `r b a`. This is essentially asserting the trichotomy law, common in ordered sets, that for any two elements, either the first precedes the second, the two are equal, or the second precedes the first.
More concisely: For any type `α` and trichotomous relation `r` on `α`, given any two elements `a` and `b`, either `r a b`, `r b a`, or `a = b` holds.
|
asymm
theorem asymm : ∀ {α : Sort u} {r : α → α → Prop} [inst : IsAsymm α r] {a b : α}, r a b → ¬r b a
This theorem states that, in any sort or type `α`, given a binary relation `r` and assuming that `r` is an asymmetric relation, for all elements `a` and `b` of `α`, if `r a b` holds, then `r b a` cannot hold. In other words, if `r` relates `a` to `b`, it cannot relate `b` back to `a`. This corresponds to the mathematical concept of asymmetric relation, where if a relation holds from `a` to `b`, it cannot hold from `b` to `a`.
More concisely: In any asymmetric relation r on type α, for all a and b, if r a b holds then r b a does not hold.
|
symm
theorem symm : ∀ {α : Sort u} {r : α → α → Prop} [inst : IsSymm α r] {a b : α}, r a b → r b a
This theorem, `symm`, states that for any type `α`, any binary relation `r` on `α`, and any two elements `a` and `b` of type `α`, if the relation `r` is symmetric (i.e., `r a b` implies `r b a` for any `a` and `b`), then if `r a b` holds, `r b a` must also hold. In other words, if `a` is related to `b` via a symmetric relation, then `b` is also related to `a` via the same relation.
More concisely: If `r` is a symmetric relation on type `α`, then for all `a` and `b` in `α`, `r a b` implies `r b a`.
|
not_lt_of_lt
theorem not_lt_of_lt : ∀ {α : Sort u} {lt : α → α → Prop} [inst : IsStrictOrder α lt] {a b : α}, lt a b → ¬lt b a := by
sorry
This theorem, "not_lt_of_lt", states that for any strictly ordered type `α` with a "less-than" relation `lt`, if a certain element `a` is less than another element `b`, then `b` cannot be less than `a`. This theorem applies to any strictly ordered set, where "strictly ordered" means that the relation is irreflexive (no element is less than itself) and transitive (if `a` is less than `b` and `b` is less than `c`, then `a` is less than `c`). This theorem captures the key property of asymmetric relations in strictly ordered sets.
More concisely: In a strictly ordered set, if `a` is less than `b`, then `b` cannot be less than `a`.
|
total_of
theorem total_of : ∀ {α : Sort u} (r : α → α → Prop) [inst : IsTotal α r] (a b : α), r a b ∨ r b a
This theorem states that for any type `α` and relation `r` on `α`, if the relation `r` is a total relation on `α` (i.e., for all elements `a` and `b` of `α`, either `r a b` or `r b a` holds true), then for any two elements `a` and `b` of `α`, either `r a b` or `r b a` is true. In terms of mathematical logic, it asserts that the relation `r` is total, meaning that for any two elements in the set, one must be related to the other or vice versa.
More concisely: If a relation on a type is total, then it is reflexive and symmetric. (In other words, for all `a` and `b` in the type, `r a b` and `r b a` hold true.)
|
trichotomous_of
theorem trichotomous_of :
∀ {α : Sort u} (r : α → α → Prop) [inst : IsTrichotomous α r] (a b : α), r a b ∨ a = b ∨ r b a
This theorem states that for any type `α` and a binary relation `r` on `α`, if `IsTrichotomous α r` is a trichotomous relation (a mathematical term meaning that for any two elements `a` and `b` of type `α`, exactly one of the following is true: `r a b`, `a = b`, or `r b a`), then for all elements `a` and `b` of the type `α`, one and only one of these possibilities must hold: `r a b`, `a = b`, or `r b a`.
More concisely: If `r` is a trichotomous relation on type `α`, then for all `a` and `b` in `α`, exactly one of `r a b`, `a = b`, or `r b a` holds.
|
refl_of
theorem refl_of : ∀ {α : Sort u} (r : α → α → Prop) [inst : IsRefl α r] (a : α), r a a
This theorem states that for any type `α` and a binary relation `r` on `α`, if `r` is reflexive (as indicated by the reflexive instance `IsRefl α r`), then `r` holds for every element `a` of type `α` with itself. In other words, for all `a` in `α`, we have `r a a`, which is the formal definition of reflexivity.
More concisely: If `r` is a reflexive binary relation on type `α`, then for all `a` in `α`, we have `r a a`.
|
antisymm
theorem antisymm : ∀ {α : Sort u} {r : α → α → Prop} [inst : IsAntisymm α r] {a b : α}, r a b → r b a → a = b := by
sorry
The theorem `antisymm` states that for any type `α` and any relation `r` on `α`, if this relation `r` is antisymmetric (i.e., for all `a` and `b` in `α`, if `r a b` and `r b a` then `a` equals `b`), then for any `a` and `b` in `α`, if `r a b` and `r b a` are both true, it follows that `a` equals `b`. In simpler words, this theorem captures the property of antisymmetry: if two elements in a set relate to each other under a certain relation, they must be the same.
More concisely: If a binary relation on a type is antisymmetric, then for all elements `a` and `b`, if `a` is related to `b` and `b` is related to `a`, then `a` equals `b`.
|
irrefl_of
theorem irrefl_of : ∀ {α : Sort u} (r : α → α → Prop) [inst : IsIrrefl α r] (a : α), ¬r a a
This theorem states that for any type `α` and a binary relation `r` on `α`, if `r` is irreflexive (as indicated by `IsIrrefl α r`), then for any element `a` of type `α`, `r a a` cannot hold. In other words, no element is related to itself under an irreflexive relation.
More concisely: For any type `α` and irreflexive binary relation `r` on `α`, there is no element `a` in `α` such that `r a a` holds.
|