WellFounded.induction
theorem WellFounded.induction :
∀ {α : Sort u} {r : α → α → Prop},
WellFounded r → ∀ {C : α → Prop} (a : α), (∀ (x : α), (∀ (y : α), r y x → C y) → C x) → C a
This theorem states that for any type `α` and a relation `r` on `α`, if `r` is well-founded, then for any predicate `C` on `α` and an element `a` of `α`, if every `x` in `α` satisfies `C` whenever all `y` related to `x` by `r` satisfy `C`, then `a` satisfies `C`. In other words, this is the principle of well-founded induction: if a property holds for all elements that are "smaller" according to a well-founded relation, then it holds for all elements.
More concisely: If `r` is a well-founded relation on type `α` and for all `a` in `α`, if every `x` related to `a` by `r` satisfies predicate `C(x)`, then `C(a)` holds.
|
WellFounded.fix_eq
theorem WellFounded.fix_eq :
∀ {α : Sort u} {C : α → Sort v} {r : α → α → Prop} (hwf : WellFounded r)
(F : (x : α) → ((y : α) → r y x → C y) → C x) (x : α), hwf.fix F x = F x fun y x => hwf.fix F y
This theorem states that for any well-founded relation `r` on a type `α`, and for any function `F` that takes an element of this type and a function (which itself takes an element `y` of type `α` and a proof that `y` is related to the original element by `r`, returning a type `C y`), and an element `x` of `α`, the well-founded fixpoint of `F` at `x` is equal to `F` applied to `x` and a function that takes `y` and a proof of `r y x`, and returns the well-funded fixpoint of `F` at `y`. In other words, it shows how the computation of `WellFounded.fix` unfolds, allowing to recursively apply `F` to smaller arguments according to the well-founded relation `r`.
More concisely: For any well-founded relation `r` on type `α` and function `F`: The well-founded fixpoint of `F` at an element `x` equals `F` applied to `x` and the well-founded fixpoint of `F` at a related `y`.
|
Prod.lex_def
theorem Prod.lex_def :
∀ {α : Type u} {β : Type v} (r : α → α → Prop) (s : β → β → Prop) {p q : α × β},
Prod.Lex r s p q ↔ r p.1 q.1 ∨ p.1 = q.1 ∧ s p.2 q.2
This theorem states that for any types `α` and `β`, and relations `r` on `α` and `s` on `β`, for any ordered pairs `p` and `q` from `α × β`, the lexicographic order `Prod.Lex r s p q` holds if and only if the relation `r` holds on the first components of `p` and `q`, or the first components of `p` and `q` are equal and the relation `s` holds on their second components. In other words, it's defining how to order pairs: first by the 'α' part, and then by the 'β' part if the 'α' parts are equal.
More concisely: For any types `α` and `β` and relations `r` on `α` and `s` on `β`, the lexicographic order `Prod.Lex r s` on `α × β` holds if and only if `r` applies to the first components of pairs and, when first components are equal, `s` applies to the second components.
|