LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Order.Grade

`GradeMinOrder.isMin_grade` theorem GradeMinOrder.isMin_grade : ∀ {𝕆 : Type u_5} {α : Type u_6} [inst : Preorder 𝕆] [inst_1 : Preorder α] [self : GradeMinOrder 𝕆 α] ⦃a : α⦄, IsMin a → IsMin (GradeOrder.grade a) The theorem `GradeMinOrder.isMin_grade` states that for any partially ordered types 𝕆 and α, given an instance of the `GradeMinOrder` structure, if a value `a` of type α is a minimal element, then the grade of 'a' is also a minimal element. In simpler terms, if 'a' is a minimal element in its context, then the grade of 'a' (calculated using the `GradeOrder.grade` function) is also minimal in its own context. More concisely: If `(α, ≤)` is a partially ordered type with a given instance of `GradeMinOrder`, and `a` is a minimal element of type α, then the grade of `a` is a minimal element in the grade order.
`CovBy.grade` theorem CovBy.grade : ∀ (𝕆 : Type u_1) {α : Type u_3} [inst : Preorder 𝕆] [inst_1 : Preorder α] [inst_2 : GradeOrder 𝕆 α] {a b : α}, a ⋖ b → grade 𝕆 a ⋖ grade 𝕆 b The theorem `CovBy.grade` states that for any types `𝕆` and `α` that have preorder structures, and any `a` and `b` of type `α`, if `a` is covered by `b` (denoted as `a ⋖ b`), then the grade of `a` is also covered by the grade of `b` (denoted as `grade 𝕆 a ⋖ grade 𝕆 b`). Here, the grade of an element in a graded order can be thought of as the number of elements you need to go down by to get to the bottom (`⊥`). This theorem therefore asserts a preservation of the covering relation under the grade function in this structure. More concisely: For any preordered types `𝕆` and `α`, if `a ⋖ b` holds in `α` then `grade 𝕆 a ⋖ grade 𝕆 b` holds in `𝕆`.
`GradeBoundedOrder.isMax_grade` theorem GradeBoundedOrder.isMax_grade : ∀ {𝕆 : Type u_5} {α : Type u_6} [inst : Preorder 𝕆] [inst_1 : Preorder α] [self : GradeBoundedOrder 𝕆 α] ⦃a : α⦄, IsMax a → IsMax (GradeOrder.grade a) The theorem `GradeBoundedOrder.isMax_grade` states that for all types `𝕆` and `α`, where `𝕆` and `α` are pre-ordered and `𝕆` is a grade bounded order of `α`, if `a` is a maximal element in `α`, then the grade of `a` is also a maximal element in `𝕆`. This means that no other element in `α` has a grade in `𝕆` that is strictly greater than the grade of `a`. More concisely: For any pre-ordered type `α` with a grade bounded order `𝕆`, if `a` is a maximal element in `α`, then the grade of `a` is a maximal element in `𝕆`. In other words, no element in `α` has a greater grade in `𝕆`.
`GradeOrder.grade_strictMono` theorem GradeOrder.grade_strictMono : ∀ {𝕆 : Type u_5} {α : Type u_6} [inst : Preorder 𝕆] [inst_1 : Preorder α] [self : GradeOrder 𝕆 α], StrictMono GradeOrder.grade The theorem `GradeOrder.grade_strictMono` states that for any types `𝕆` and `α` that are preordered, if `GradeOrder` is defined on `𝕆` and `α`, then the `grade` function which maps elements from type `α` to `𝕆` is strictly monotonic. In other words, for any two elements `a` and `b` in `α` where `a < b`, we always have `grade(a) < grade(b)`. More concisely: For any preordered types `𝕆` and `α` with defined `GradeOrder`, the grade function `grade : α → 𝕆` is strictly monotonic, i.e., `grade(a) < grade(b)` for all `a < b` in `α`.
`GradeMaxOrder.isMax_grade` theorem GradeMaxOrder.isMax_grade : ∀ {𝕆 : Type u_5} {α : Type u_6} [inst : Preorder 𝕆] [inst_1 : Preorder α] [self : GradeMaxOrder 𝕆 α] ⦃a : α⦄, IsMax a → IsMax (GradeOrder.grade a) The theorem `GradeMaxOrder.isMax_grade` states that for any types `𝕆` and `α` having a preorder relation and a `GradeMaxOrder` relation, if `a` is a maximal element in the set of `α` (i.e., no element in `α` is strictly greater than `a`), then the grade of `a` (obtained through the `GradeOrder.grade` function) is also a maximal element in the set of `𝕆`. This theorem essentially describes a preservation of maximality under the grading function in the context of preordered sets. More concisely: If `a` is a maximal element in a preordered set `(α, ≤)` with a `GradeMaxOrder`, then the grade of `a` (obtained through the `GradeOrder.grade` function) is a maximal element in the preorder `(𝕆, ≤)`.
`IsMin.grade` theorem IsMin.grade : ∀ (𝕆 : Type u_1) {α : Type u_3} [inst : Preorder α] [inst_1 : Preorder 𝕆] [inst_2 : GradeMinOrder 𝕆 α] {a : α}, IsMin a → IsMin (grade 𝕆 a) This theorem states that for any types `𝕆` and `α`, where `α` is a preorder and `𝕆` is a preorder, and under the condition that `𝕆` and `α` have a grade-minimal order, if `a` is a minimal element in `α`, then the grade of `a` is also a minimal element in `𝕆`. In simpler terms, if `a` is the smallest element according to the order defined for `α`, then the number of steps you would need to go down to get to the bottom of the order for `𝕆` is also the smallest possible. More concisely: If `α` is a preordered type with a grade-minimal order and `a` is a minimal element in `α`, then the grade of `a` is a minimal element in the preorder `𝕆` on types.
`IsMax.grade` theorem IsMax.grade : ∀ (𝕆 : Type u_1) {α : Type u_3} [inst : Preorder α] [inst_1 : Preorder 𝕆] [inst_2 : GradeMaxOrder 𝕆 α] {a : α}, IsMax a → IsMax (grade 𝕆 a) The theorem `IsMax.grade` states that for any type `𝕆`, for any type `α` that is a preordered set, and for any instance of `GradeMaxOrder` relating `𝕆` and `α`, if a given element `a` of type `α` is a maximal element (i.e., no other element in `α` is strictly greater than `a`), then the grade (which, by analogy, is the number of elements one needs to descend to reach the minimal element) of `a` is also a maximal element. More concisely: If `α` is a preordered set over type `𝕆` with maximal element `a`, then the grade of `a` is a maximal element among the grades of elements in `α`.
`GradeOrder.covBy_grade` theorem GradeOrder.covBy_grade : ∀ {𝕆 : Type u_5} {α : Type u_6} [inst : Preorder 𝕆] [inst_1 : Preorder α] [self : GradeOrder 𝕆 α] ⦃a b : α⦄, a ⋖ b → GradeOrder.grade a ⋖ GradeOrder.grade b The theorem `GradeOrder.covBy_grade` states that for any types `𝕆` and `α` endowed with a preorder structure, and an instance `GradeOrder 𝕆 α`, if an element `a` of type `α` is covered by another element `b` of type `α` (denoted `a ⋖ b`), then the grade of `a` is also covered by the grade of `b` (denoted `GradeOrder.grade a ⋖ GradeOrder.grade b`). In other words, the grading function `GradeOrder.grade` preserves the cover relation. More concisely: For any type endowed with a preorder structure and a GradeOrder instance, if an element is covered by another element, then the grades of the elements have a cover relation.
`grade_strictMono` theorem grade_strictMono : ∀ {𝕆 : Type u_1} {α : Type u_3} [inst : Preorder 𝕆] [inst_1 : Preorder α] [inst_2 : GradeOrder 𝕆 α], StrictMono (grade 𝕆) The theorem `grade_strictMono` states that for any types `𝕆` and `α`, with `𝕆` and `α` being preordered and `𝕆` being a graded order over `α`, the `grade` function, which assigns to each element of `α` its grade in `𝕆`, is strictly monotone. This means that if `a` and `b` are elements of `α` and `a < b`, then `grade 𝕆 a < grade 𝕆 b`. In other words, if one element in `α` is less than another, its grade, i.e., the number of elements you need to go down by to get to the bottom, is also less. More concisely: For any preordered type `α` with a graded order `𝕆`, the grade function strictly increases along `<`-chains in `α`.