mul_kstar_le_self
theorem mul_kstar_le_self : ∀ {α : Type u_1} [inst : KleeneAlgebra α] {a b : α}, b * a ≤ b → b * KStar.kstar a ≤ b := by
sorry
This theorem, `mul_kstar_le_self`, states that for any type `α` that is a Kleene algebra, and for any elements `a` and `b` of that type, if the multiplication of `b` and `a` is less than or equal to `b`, then the multiplication of `b` and the `kstar` of `a` (a method from the Kleene algebra involving `a`) is also less than or equal to `b`.
More concisely: For any Kleene algebra type `α` and elements `a, b` of `α`, if `b` * `a` ≤ `b`, then `b` * (`kstar` `a`) ≤ `b`.
|
mul_kstar_le_kstar
theorem mul_kstar_le_kstar : ∀ {α : Type u_1} [inst : KleeneAlgebra α] {a : α}, a * KStar.kstar a ≤ KStar.kstar a := by
sorry
The theorem `mul_kstar_le_kstar` states that for any type `α` that forms a Kleene algebra, and for any element `a` of type `α`, the product of `a` and the Kleene star of `a` (denoted as `a * KStar.kstar a`) is less than or equal to the Kleene star of `a` (denoted as `KStar.kstar a`). In the context of Kleene algebras, the "less than or equal to" relation typically represents an ordering based on possible reachability or effect in a system modeled by the algebra.
More concisely: For any element `a` in a Kleene algebra `α`, `a * KStar.kstar a ≤ KStar.kstar a`.
|
LE.le.add_eq_right
theorem LE.le.add_eq_right : ∀ {α : Type u_1} [inst : IdemSemiring α] {a b : α}, a ≤ b → a + b = b
This theorem, `LE.le.add_eq_right`, is an alias for the reverse direction of `add_eq_right_iff_le`. It states that for any idempotent semiring `α` and any elements `a` and `b` from `α`, if `a` is less than or equal to `b`, then the sum of `a` and `b` is equal to `b`. In the context of this theorem, an idempotent semiring is a semiring (a set equipped with two binary operations satisfying certain properties) where the multiplication operation is idempotent (i.e., for any element `x`, `x * x = x`).
More concisely: For any idempotent semiring `α` and elements `a` and `b` from `α`, if `a ≤ b`, then `a + b = b`.
|
kstar_le_of_mul_le_left
theorem kstar_le_of_mul_le_left :
∀ {α : Type u_1} [inst : KleeneAlgebra α] {a b : α}, 1 ≤ b → b * a ≤ b → KStar.kstar a ≤ b
The theorem `kstar_le_of_mul_le_left` is a statement about elements in a Kleene algebra, which is represented by the type variable `α`. Given any two elements `a` and `b` of this Kleene algebra, the theorem states that if the unit element `1` is less than or equal to `b` and the product `b * a` is also less than or equal to `b`, then it follows that the Kleene star of `a` (denoted by `KStar.kstar a`) is less than or equal to `b`. The Kleene star operation is a unary operation widely used in the theory of formal languages and automata, which in this context can be seen as a kind of "closure" operation.
More concisely: If `1 ≤ b` and `b * a ≤ b` hold in a Kleene algebra, then `KStar.kstar a ≤ b`.
|
LE.le.add_eq_left
theorem LE.le.add_eq_left : ∀ {α : Type u_1} [inst : IdemSemiring α] {a b : α}, b ≤ a → a + b = a
This theorem, named `LE.le.add_eq_left`, states that for any idempotent semiring `α` and any two elements `a` and `b` of this semiring, if `b` is less than or equal to `a`, then the result of adding `a` and `b` equals `a`. In other words, in such a semiring, if `b` is less than or equal to `a`, adding `b` to `a` does not change the value of `a`.
More concisely: In an idempotent semiring, if `b` is less than or equal to `a`, then `a + b = a`.
|
one_le_kstar
theorem one_le_kstar : ∀ {α : Type u_1} [inst : KleeneAlgebra α] {a : α}, 1 ≤ KStar.kstar a
The theorem `one_le_kstar` states that for any given type `α` which is an instance of `KleeneAlgebra`, and for any element `a` of type `α`, `1` is less than or equal to `kstar` of `a`. Here, `KStar.kstar` is a function that takes an element from the Kleene algebra and returns an element of the same type. The comparison `1 ≤ KStar.kstar a` is made with respect to the partial order defined by the Kleene algebra structure on `α`.
More concisely: For any element `a` in a Kleene algebra `α`, `1` is less than or equal to the Kleene star operation `kstar` applied to `a`. In mathematical notation: `1 ≤ KStar.kstar a`.
|
kstar_mul_le_self
theorem kstar_mul_le_self : ∀ {α : Type u_1} [inst : KleeneAlgebra α] {a b : α}, a * b ≤ b → KStar.kstar a * b ≤ b := by
sorry
The theorem `kstar_mul_le_self` states that for all types `α` that are instances of the `KleeneAlgebra`, and for all elements `a` and `b` of this type `α`, if `a * b` is less than or equal to `b`, then the `kstar` of `a` multiplied by `b` is also less than or equal to `b`. Here, `KStar.kstar a` refers to the operation `kstar` applied to `a`, where `kstar` is a function associated with the `KStar` class in the Kleene algebra context, often representing the reflexive-transitive closure in the language of regular expressions or formal language theory.
More concisely: For all types `α` in the Kleene Algebra and all elements `a, b` of `α`, if `a * b ≤ b`, then `KStar.kstar a * b ≤ b`.
|
kstar_mul_le_kstar
theorem kstar_mul_le_kstar : ∀ {α : Type u_1} [inst : KleeneAlgebra α] {a : α}, KStar.kstar a * a ≤ KStar.kstar a := by
sorry
This theorem, `kstar_mul_le_kstar`, states that for any type `α` that is an instance of a Kleene Algebra, and any element `a` of `α`, the result of multiplying the Kleene star of `a` (`KStar.kstar a`) with `a`, is less than or equal to the Kleene star of `a`. In mathematical terms, for any `a` in a Kleene algebra, we have that $KStar(a) * a \leq KStar(a)$.
More concisely: For any element `a` in a Kleene algebra, $KStar(a) \cdot a \leq KStar(a)$.
|
add_eq_sup
theorem add_eq_sup : ∀ {α : Type u_1} [inst : IdemSemiring α] (a b : α), a + b = a ⊔ b
This theorem, `add_eq_sup`, states that for any type `α` that forms an idempotent semiring (denoted by `IdemSemiring α`), the sum of any two elements `a` and `b` of this type is equivalent to the supremum (greatest element) of `a` and `b`. In the context of idempotent semiring, the addition operation behaves as taking the maximum of the two elements. This holds for all `a` and `b` in the given idempotent semiring.
More concisely: For any idempotent semiring `α`, the addition of two elements `a` and `b` is equal to the supremum of `a` and `b`.
|
le_kstar
theorem le_kstar : ∀ {α : Type u_1} [inst : KleeneAlgebra α] {a : α}, a ≤ KStar.kstar a
The theorem `le_kstar` states that for any type `α` that forms a Kleene algebra, and for any element `a` of that type, `a` is less than or equal to `KStar.kstar a`. Here, "less than or equal to" is interpreted in the sense of the partial order defined on the Kleene algebra. The function `KStar.kstar` represents the Kleene star operation, which is a unary operation in the algebra.
More concisely: For any Kleene algebra type `α` and element `a` in `α`, `a ≤ KStar.kstar a`.
|