Language.reverse_involutive
theorem Language.reverse_involutive : ∀ {α : Type u_1}, Function.Involutive Language.reverse
This theorem states that the operation of reversing a language is involutive for any type `α`. In other words, if we take a language, reverse it, and then reverse it again, we get back the original language. In more formal terms, for all types `α`, applying the `Language.reverse` function twice to any language results in the original language. This is equivalent to saying that the `Language.reverse` function is its own inverse with respect to function composition.
More concisely: For any type `α`, the operation of reversing a language using `Language.reverse` is an involution. In other words, `Language.reverse ∘ Language.reverse` equals the identity function for languages.
|
Language.mul_iSup
theorem Language.mul_iSup :
∀ {α : Type u_1} {ι : Sort v} (l : ι → Language α) (m : Language α), m * ⨆ i, l i = ⨆ i, m * l i
This theorem, `Language.mul_iSup`, states that for any type `α`, any type `ι`, any function `l` from `ι` to a Language of `α`, and any Language `m` of `α`, the product of `m` and the supremum (or the union in the context of sets of languages) over `i` of `l i` equals the supremum over `i` of the product of `m` and `l i`. In other words, it is asserting that the operation of "multiplying" a language with the supremum of a set of languages distributes over the set of languages.
More concisely: For any type `α`, any type `ι`, any function `l` from `ι` to a Language of `α`, and any Langages `m` and `n` of `α`, the supremum of `{mi \* li : i ∈ ι}` equals `m * (sup i, li)`.
|
Language.kstar_eq_iSup_pow
theorem Language.kstar_eq_iSup_pow : ∀ {α : Type u_1} (l : Language α), KStar.kstar l = ⨆ i, l ^ i
This theorem states that for any given language `l` over an alphabet of type `α`, the Kleene star operation on `l` is equivalent to the supremum of `l` raised to every natural number `i`. In other words, the set of all strings that can be formed by concatenating zero or more strings from `l` (which is what `KStar.kstar l` denotes) is the same as the union of all sets of strings that can be formed by concatenating `i` strings from `l` for every non-negative integer `i` (which is what `⨆ i, l ^ i` denotes).
More concisely: For any language `l` over an alphabet `α`, the Kleene star operation `KStar.kstar l` is equal to the supremum `⨆ i, l ^ i` of all powers of `l`.
|
Language.ext
theorem Language.ext : ∀ {α : Type u_1} {l m : Language α}, (∀ (x : List α), x ∈ l ↔ x ∈ m) → l = m
The theorem `Language.ext` states that for any type `α` and any two languages `l` and `m` over this type, if for every list of elements of type `α` the condition that this list is in language `l` is equivalent to the condition that this list is in language `m`, then the languages `l` and `m` are indeed the same. In other words, two languages are equal if and only if they contain exactly the same lists of elements.
More concisely: Two languages over a type are equal if and only if they contain the same lists of elements.
|