instPartialOrderAntisymmetrization.proof_1
theorem instPartialOrderAntisymmetrization.proof_1 :
∀ {α : Type u_1} [inst : Preorder α] (x x_1 x_2 x_3 : α),
Setoid.r x x_2 → Setoid.r x_1 x_3 → (x ≤ x_1) = (x_2 ≤ x_3)
This theorem states that for any type `α` that is preordered (denoted as `inst : Preorder α`), and for any four elements `x`, `x_1`, `x_2`, `x_3` of this type, if `x` is equivalent to `x_2` and `x_1` is equivalent to `x_3` (as per the equivalence relation of a setoid, denoted as `Setoid.r`), then the statement "`x` is less than or equal to `x_1`" (denoted as `x ≤ x_1`) is equivalent to the statement "`x_2` is less than or equal to `x_3`" (denoted as `x_2 ≤ x_3`). In other words, the order relationship between `x` and `x_1` is the same as the order relationship between `x_2` and `x_3` when `x` is equivalent to `x_2` and `x_1` is equivalent to `x_3`.
More concisely: For any preordered type `α` and elements `x`, `x_1`, `x_2`, `x_3` of `α` such that `x ≈ x_2` and `x_1 ≈ x_3` (where `≈` is the equivalence relation of a setoid), the order relationship `x ≤ x_1` holds if and only if `x_2 ≤ x_3`.
|
AntisymmRel.eq
theorem AntisymmRel.eq :
∀ {α : Type u_1} {r : α → α → Prop} [inst : IsRefl α r] [inst : IsAntisymm α r] {a b : α},
AntisymmRel r a b → a = b
This theorem, `AntisymmRel.eq`, is stating that for any type `α` and a binary relation `r` on `α`, if `r` is reflexive (meaning that each element is related to itself) and antisymmetric (meaning that if `a` is related to `b` and `b` is related to `a`, then `a` must be equal to `b`), then if the antisymmetrization relation (`AntisymmRel`) holds between two elements `a` and `b`, it follows that `a` is equal to `b`.
More concisely: If a binary relation on a type is reflexive and antisymmetric, then the antisymmetric relation implies equality.
|
AntisymmRel.symm
theorem AntisymmRel.symm : ∀ {α : Type u_1} {r : α → α → Prop} {a b : α}, AntisymmRel r a b → AntisymmRel r b a := by
sorry
This theorem states that for any type `α` and any relation `r` on `α`, the antisymmetrization of `r` is symmetric. In other words, if `r` is a relation on some type `α` and `a` and `b` are elements of `α` such that `r` holds between `a` and `b` and between `b` and `a` (i.e., the antisymmetrization of `r` holds between `a` and `b`), then the antisymmetrization of `r` also holds between `b` and `a`.
More concisely: If a relation `r` on type `α` is antisymmetric, then it is symmetric. That is, for all `a` and `b` in `α`, if `r` holds between `a` and `b` and `b` and `a`, then `a` is equal to `b`.
|