Relation.acc_of_singleton
theorem Relation.acc_of_singleton :
∀ {α : Type u_1} {r : α → α → Prop} [inst : IsIrrefl α r] {s : Multiset α},
(∀ a ∈ s, Acc (Relation.CutExpand r) {a}) → Acc (Relation.CutExpand r) s
This theorem states that a multiset, in the context of a given irreflexive relation `r`, is accessible under the operation `CutExpand` if all its singleton subsets are also accessible under `CutExpand`. Here, `Multiset α` is a type representing a set with duplicates allowed (essentially a list of terms of type `α`), `Acc` denotes an accessible point in a relation, and `CutExpand` is an operation on the relation. The irreflexivity of `r` means that for any element `a` of type `α`, `r a a` is false. The theorem is parameterized over any type `α` and a relation `r` on `α`.
More concisely: If all singleton subsets of a multiset are accessible under `CutExpand` in an irreflexive relation, then the multiset is accessible under `CutExpand` in that relation.
|
Relation.cutExpand_fibration
theorem Relation.cutExpand_fibration :
∀ {α : Type u_1} (r : α → α → Prop),
Relation.Fibration (Prod.GameAdd (Relation.CutExpand r) (Relation.CutExpand r)) (Relation.CutExpand r) fun s =>
s.1 + s.2
The theorem `Relation.cutExpand_fibration` states that for any relation `r` on a type `α`, the operation of multiset addition, which takes a pair of multisets and produces a multiset, is a fibration between the game sum of the expanded cut of `r` with itself and the expanded cut of `r` itself. In other words, for any pair of elements from the multisets, if they are related by the expanded cut of `r`, then there exists an element from the first multiset such that it is related to the first element by the game sum of the expanded cut of `r`, and the sum of this element and the second element from the pair equals the second element of the pair.
More concisely: For any relation `r` on a type `α`, the multiset addition operation is a fibration between the game sum of the expanded cuts of `r` and the expanded cut of `r`, meaning that if two elements are related by the expanded cut of `r`, there exists an element from the first multiset related to the first element by the game sum of the expanded cut of `r` such that their sum equals the second element.
|
Acc.cutExpand
theorem Acc.cutExpand :
∀ {α : Type u_1} {r : α → α → Prop} [inst : IsIrrefl α r] {a : α}, Acc r a → Acc (Relation.CutExpand r) {a} := by
sorry
This theorem states that for any type `α` and any relation `r` on `α` that is irreflexive, if `a` (an element of `α`) is accessible under `r`, then the singleton set `{a}` is also accessible under the `CutExpand` of `r`. Here `Acc` stands for Accessibility, `CutExpand` is a operation on relations, and `IsIrrefl` checks if a relation is irreflexive. Essentially, if an element is accessible in a relation, then this single-element set is also accessible under the expanded cut of that relation, given that the relation is irreflexive.
More concisely: For any irreflexive relation `r` on type `α` and any accessible element `a` in `α`, the singleton set `{a}` is accessible under the `CutExpand` of `r`.
|
WellFounded.cutExpand
theorem WellFounded.cutExpand :
∀ {α : Type u_1} {r : α → α → Prop}, WellFounded r → WellFounded (Relation.CutExpand r)
This theorem states that the "CutExpand" of a relation `r` on a type `α` is well-founded if `r` itself is well-founded. In mathematical terms, "well-founded" refers to a relation that does not contain any infinite descending chains. In the context of the Lean 4 theorem prover, a well-founded type allows for the usage of recursion and induction on the type. The "CutExpand" of a relation `r` is a relation that captures the concept of a 'cut', which is a division of a domain into two disjoint, nonempty parts. Thus, if the original relation `r` is well-founded, so is its CutExpand.
More concisely: If a relation on a type is well-founded, then its CutExpand relation is also well-founded.
|