Cycle.induction_on
theorem Cycle.induction_on :
∀ {α : Type u_1} {C : Cycle α → Prop} (s : Cycle α),
C Cycle.nil → (∀ (a : α) (l : List α), C ↑l → C ↑(a :: l)) → C s
This theorem is an induction principle for `Cycle`. For a given type `α` and a function `C` that assigns a property to each `Cycle α`, if `C` holds for the unique empty cycle (`Cycle.nil`), and if for any element `a : α` and list `l : List α` the property `C` holding for `l` implies `C` holding for the cycle with `a` added to `l`, then the property `C` holds for any cycle `s : Cycle α`. This theorem can be used for proving properties that hold for all cycles, and can be invoked as `induction s using Cycle.induction_on`.
More concisely: If a property `C` holds for the empty cycle and is closed under the addition of an element to a list, then `C` holds for any cycle.
|
Mathlib.Data.List.Cycle._auxLemma.10
theorem Mathlib.Data.List.Cycle._auxLemma.10 : ∀ {α : Type u_1} {a : α} {l : List α}, (a ∈ ↑l) = (a ∈ l)
This theorem, `Mathlib.Data.List.Cycle._auxLemma.10`, asserts that for any type `α`, any element `a` of this type, and any list `l` of elements of this type, checking whether `a` is in the list `l` coalesced into a set (i.e., `↑l`) is equivalent to checking whether `a` is in the list `l`. In other words, set membership and list membership are equivalent for a given element and a list in Lean.
More concisely: For any type `α`, element `a` of `α`, and list `l` of elements of `α`, the set `{x : α | x ∈ l}` containing elements of `α` that are in `l` is equal to `{a | a ∈ l}`.
|
Cycle.nodup_reverse_iff
theorem Cycle.nodup_reverse_iff : ∀ {α : Type u_1} {s : Cycle α}, s.reverse.Nodup ↔ s.Nodup
The theorem `Cycle.nodup_reverse_iff` states that for any type `α` and any cycle `s` of type `α`, the cycle `s` has no duplicates if and only if the reverse of `s` also has no duplicates. In other words, reversing a cycle does not change its duplicate-free status. This is true for all cycles, irrespective of their element types.
More concisely: For any cycle `s` of type `α`, `s` has no duplicates if and only if the reversed cycle of `s` has no duplicates.
|
List.nextOr_eq_nextOr_of_mem_of_ne
theorem List.nextOr_eq_nextOr_of_mem_of_ne :
∀ {α : Type u_1} [inst : DecidableEq α] (xs : List α) (x d d' : α) (x_mem : x ∈ xs),
x ≠ xs.getLast ⋯ → xs.nextOr x d = xs.nextOr x d'
The theorem `List.nextOr_eq_nextOr_of_mem_of_ne` states that for any type `α` with decidable equality, given a list `xs` of type `α` and three elements `x`, `d`, and `d'` of the same type, if `x` is a member of `xs` and `x` is not equal to the last element of `xs`, then the `nextOr` function applied to `x` with default value `d` is equal to the `nextOr` function applied to `x` with default value `d'`. Essentially, this theorem shows that the output of the `nextOr` function does not depend on the default values if the next value after `x` in the list exists.
More concisely: For any type `α` with decidable equality, if `x` is a non-last member of list `xs` of type `α`, then `List.nextOr x d = List.nextOr x d'`, where `d` and `d'` are default values.
|
Cycle.chain_mono
theorem Cycle.chain_mono : ∀ {α : Type u_1}, Monotone Cycle.Chain
The theorem `Cycle.chain_mono` asserts that for any type `α`, the function `Cycle.Chain` is monotonic. Monotonicity, in this context, means that if we have two relations `R` and `S` such that `R` is less than or equal to `S` (in the sense that whenever `R a b` holds, `S a b` also holds), then `Cycle.Chain R` is less than or equal to `Cycle.Chain S`. That is, if a cycle satisfies the relation `R` between its adjacent elements, then it also satisfies the relation `S` between its adjacent elements.
More concisely: For any relations R and S on a type α with R ≤ S, the cycle relation Chain(R) is less than or equal to Chain(S), i.e., if a cycle satisfies R between adjacent elements, then it also satisfies S.
|
List.nextOr_cons_of_ne
theorem List.nextOr_cons_of_ne :
∀ {α : Type u_1} [inst : DecidableEq α] (xs : List α) (y x d : α), x ≠ y → (y :: xs).nextOr x d = xs.nextOr x d
This theorem, `List.nextOr_cons_of_ne`, states that for any type `α` with decidable equality, given a list `xs` of type `α`, and three elements `y`, `x`, and `d` of type `α`, if `x` is not equal to `y`, then the `nextOr` function, when applied to the list that results from consing `y` onto `xs` (i.e., `y :: xs`), `x`, and `d`, will return the same result as the `nextOr` function applied to `xs`, `x`, and `d`. In other words, if `x` is different from the head of the list, the result of `nextOr` doesn't change when we add an element to the head of the list.
More concisely: For any type `α` with decidable equality, if list `xs` of type `α`, elements `y`, `x`, and `d` of type `α`, and `x ≠ y`, then `List.nextOr _ (y :: xs) x d` equals `List.nextOr xs x d`.
|
Cycle.chain_coe_cons
theorem Cycle.chain_coe_cons :
∀ {α : Type u_1} (r : α → α → Prop) (a : α) (l : List α), Cycle.Chain r ↑(a :: l) ↔ List.Chain r a (l ++ [a]) := by
sorry
This theorem, `Cycle.chain_coe_cons`, states that for any type `α`, relation `r` over `α`, element `a` of type `α`, and a list `l` of elements of type `α`, the property `Cycle.Chain` holding for the cycle formed by appending `a` to the front of `l` is equivalent to the property `List.Chain` holding for the list formed by appending `a` to the end of `l`. In other words, a cycle `a :: l` has the chain property with respect to `r` if and only if the list `l ++ [a]` does. This property checks if the relation `r` holds between adjacent elements of the cycle or list.
More concisely: For any type `α`, relation `r` over `α`, element `a` of type `α`, and list `l` of elements of type `α`, the cycle `[a] ++ l` has the chain property with respect to `r` if and only if the list `l ++ [a]` does.
|
Mathlib.Data.List.Cycle._auxLemma.30
theorem Mathlib.Data.List.Cycle._auxLemma.30 : ∀ {α : Type u_1} {l : List α}, (↑l).Nodup = l.Nodup
This theorem, named `Mathlib.Data.List.Cycle._auxLemma.30`, states that for any type `α` and any list of elements of this type `l`, the property of having no duplicates in the cycle form of `l` (denoted by `Cycle.Nodup ↑l`) is equivalent to the property of having no duplicates in `l` directly (denoted by `List.Nodup l`). In other words, a list `l` has no duplicate elements if and only if the cycle form of `l` also has no duplicate elements.
More concisely: The theorem `Mathlib.Data.List.Cycle._auxLemma.30` in Lean 4 states that a list `l` has no duplicate elements if and only if its cycle form also has no duplicate elements.
|
Mathlib.Data.List.Cycle._auxLemma.11
theorem Mathlib.Data.List.Cycle._auxLemma.11 : ∀ {α : Type u_1} (a : α), (a ∈ Cycle.nil) = False
This theorem, called `Mathlib.Data.List.Cycle._auxLemma.11`, states that for any type `α` and any element `a` of type `α`, `a` is not in `Cycle.nil`. In other words, there are no elements in the unique empty cycle, `Cycle.nil`. This theorem applies to all types, denoted here by `α`.
More concisely: There are no elements in the empty cycle.
|
Mathlib.Data.List.Cycle._auxLemma.9
theorem Mathlib.Data.List.Cycle._auxLemma.9 : ∀ {α : Type u_1} (l : List α), (↑l = Cycle.nil) = (l = [])
This theorem states that for any type `α` and a list `l` of type `α`, the list `l` casted to a `Cycle` type is equal to the unique empty cycle if and only if the list `l` is an empty list. In other words, a list is empty if and only if its corresponding cycle representation is also empty.
More concisely: For any type `α`, the list `l` of type `α` is empty if and only if the associated `Cycle` type representation of `l` is the empty cycle.
|