WellFounded.isAsymm
theorem WellFounded.isAsymm : ∀ {α : Type u_1} {r : α → α → Prop}, WellFounded r → IsAsymm α r
This theorem states that for any type `α` and any relation `r` on `α`, if `r` is well-founded, then `r` is also asymmetric. In other words, if `r` is a relation such that there are no infinite descending chains, then for any two elements `a` and `b` of `α`, if `a` relates to `b` and `b` relates to `a`, then `a` and `b` must be the same. This is a statement about the properties of well-founded relations in set theory.
More concisely: If `r` is a well-founded relation on type `α`, then `r` is asymmetric.
|
WellFounded.wellFounded_iff_has_min
theorem WellFounded.wellFounded_iff_has_min :
∀ {α : Type u_1} {r : α → α → Prop}, WellFounded r ↔ ∀ (s : Set α), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m := by
sorry
The theorem `WellFounded.wellFounded_iff_has_min` states that for any type `α` and relation `r`, the relation `r` is well-founded if and only if for every non-empty set `s` of type `α`, there exists an element `m` in `s` such that there is no `x` in `s` for which the relation `r` holds between `x` and `m`. In simpler terms, a relation is well-founded if every non-empty set has a minimal element under that relation, where a minimal element is one which is not related by `r` to any other element in the set.
More concisely: A relation over a type is well-founded if and only if every non-empty subset has a minimal element with respect to that relation.
|
WellFounded.min_mem
theorem WellFounded.min_mem :
∀ {α : Type u_1} {r : α → α → Prop} (H : WellFounded r) (s : Set α) (h : s.Nonempty), H.min s h ∈ s
The theorem `WellFounded.min_mem` states that for any type `α`, binary relation `r` on `α`, and a set `s` of type `α`, if `r` is a well-founded relation (i.e., there are no infinite decreasing sequences) and `s` is a nonempty set, then the minimal element of `s` under the relation `r` (as provided by `WellFounded.min`) is an element of `s`. This asserts the existence of the minimal element in the set `s` under the well-founded relation `r`.
More concisely: If `α` is a type, `r` is a well-founded relation on `α`, and `s ≠ ∅` is a subset of `α`, then there exists an `x ∈ s` such that for all `y ∈ s`, `x r y`.
|
Function.argminOn_le
theorem Function.argminOn_le :
∀ {α : Type u_1} {β : Type u_2} (f : α → β) [inst : LinearOrder β] (h : WellFounded fun x x_1 => x < x_1)
(s : Set α) {a : α} (ha : a ∈ s) (hs : optParam s.Nonempty ⋯), f (Function.argminOn f h s hs) ≤ f a
The theorem `Function.argminOn_le` states that for any types `α` and `β`, a function `f` from `α` to `β`, and a non-empty set `s` of `α`, if `β` has a linear order and well-foundedness property, then the function value at the element of `s` that minimizes the function `f` (determined by `Function.argminOn`) is less than or equal to the function value at any other element of `s`. This means that for any given element `a` in the set `s`, the value of `f` at `Function.argminOn f h s hs` is always less than or equal to the value of `f` at `a`.
More concisely: For any non-empty set `s` and function `f` from a type `α` to a linearly ordered and well-founded type `β`, the minimum value of `f` in `s` (as defined by `Function.argminOn`) is less than or equal to the value of `f` at any other element in `s`.
|
WellFounded.has_min
theorem WellFounded.has_min :
∀ {α : Type u_4} {r : α → α → Prop}, WellFounded r → ∀ (s : Set α), s.Nonempty → ∃ a ∈ s, ∀ x ∈ s, ¬r x a := by
sorry
The theorem `WellFounded.has_min` states that for any type `α` and any relation `r` on `α`, if `r` is a well-founded relation, then every non-empty set of `α` has a minimal element according to `r`. In other words, given a well-founded relation `r` and a non-empty set `s`, there exists an element `a` in `s` such that, for all other elements `x` in `s`, the relation `r` does not hold from `x` to `a`. This effectively means that `a` is a minimum element of the set `s` with respect to the relation `r`.
More concisely: If `α` is a type and `r` is a well-founded relation on `α`, then every non-empty subset of `α` has a minimal element with respect to `r`.
|
Acc.induction_bot
theorem Acc.induction_bot :
∀ {α : Sort u_4} {r : α → α → Prop} {a bot : α},
Acc r a → ∀ {C : α → Prop}, (∀ (b : α), b ≠ bot → C b → ∃ c, r c b ∧ C c) → C a → C bot
The theorem `Acc.induction_bot` is a principle of induction for well-founded relations, which states the following: for a given type `α`, a relation `r` on `α`, a property `C : α → Prop`, and elements `a` and `bot` of `α`, if `a` is accessible by `r` and for each element `b` (not equal to `bot`) that satisfies the property `C`, there exists another element `c` such that `r c b` and `C c` hold, then if `C a` holds, `C bot` also holds. Essentially, it enables us to apply induction in a scenario where we start from some `a` and proceed towards `bot` in the relation `r`, under certain conditions.
More concisely: If `r` is a well-founded relation on `α`, `C : α → Prop`, `a` is accessible from `bot` via `r`, and `C a` holds, then `C bot` holds.
|
WellFounded.induction_bot'
theorem WellFounded.induction_bot' :
∀ {α : Sort u_4} {β : Sort u_5} {r : α → α → Prop},
WellFounded r →
∀ {a bot : α} {C : β → Prop} {f : α → β},
(∀ (b : α), f b ≠ f bot → C (f b) → ∃ c, r c b ∧ C (f c)) → C (f a) → C (f bot)
This theorem, `WellFounded.induction_bot'`, is an induction principle for well-founded relations. Given a well-founded relation `r` on a type `α`, a function `f` from `α` to another type `β`, a property `C` defined on `β`, and two elements `a` and `bot` of `α`, the theorem asserts that if the property `C` holds for `f(a)`, and for every `b` in `α` such that `f(b)` is not equal to `f(bot)` and `C(f(b))` holds, there exists a `c` such that `r(c, b)` holds and `C(f(c))` holds, then it must also be the case that `C(f(bot))` holds.
More concisely: If `r` is a well-founded relation on type `α`, `f: α -> β`, `C: β -> Prop`, `a, bot ∈ α`, and for all `b ≠ bot`, `C(f(b))` implies the existence of a `c` with `r(c, b)` and `C(f(c))`, then `C(f(bot))` holds.
|
WellFounded.induction_bot
theorem WellFounded.induction_bot :
∀ {α : Sort u_4} {r : α → α → Prop},
WellFounded r → ∀ {a bot : α} {C : α → Prop}, (∀ (b : α), b ≠ bot → C b → ∃ c, r c b ∧ C c) → C a → C bot
This theorem, named `WellFounded.induction_bot`, is an induction principle related to well-founded relations. Given a well-founded relation `r` on a type `α`, a predicate `C : α → Prop`, and an element `bot : α`, it proves that if `C a` holds for some `a` and for every element `b` for which `C b` holds there exists an element `c` such that `r c b` and `C c` are true, then `C bot` also holds. This is useful when `r` is a transitive relation, as the theorem essentially establishes `bot` as the smallest element with respect to `r` for which `C` is true.
More concisely: If `r` is a well-founded relation on type `α`, `C : α → Prop`, and `bot : α` satisfy `C a` for some `a` and for all `b` with `C b` there exists `c` with `r c b` and `C c`, then `C bot` holds.
|
WellFounded.mono
theorem WellFounded.mono :
∀ {α : Type u_1} {r r' : α → α → Prop}, WellFounded r → (∀ (a b : α), r' a b → r a b) → WellFounded r'
This theorem, `WellFounded.mono`, states that for any type `α` and any two binary relations `r` and `r'` on `α`, if `r` is a well-founded relation (i.e., it does not have any infinite descending chains) and for all `a` and `b` in `α`, `r' a b` implies `r a b`, then `r'` is also a well-founded relation. In other words, the well-foundedness of a relation can be transferred to another relation if the second relation is a subset of the first.
More concisely: If `r` is a well-founded relation on type `α` and `r'` is a relation on `α` such that `r' ⊆ r`, then `r'` is also well-founded.
|
WellFounded.isIrrefl
theorem WellFounded.isIrrefl : ∀ {α : Type u_1} {r : α → α → Prop}, WellFounded r → IsIrrefl α r
This theorem states that for any type `α` and any relation `r` over `α`, if `r` is well-founded, then it is also irreflexive. In other words, there are no elements `a` in `α` for which `r a a` holds true. In the context of set theory, a relation is well-founded if there are no infinite descending chains, and is irreflexive if no element is related to itself.
More concisely: If `α` is a type and `r` is a well-founded relation over `α`, then `r` is irreflexive.
|
WellFounded.not_lt_min
theorem WellFounded.not_lt_min :
∀ {α : Type u_1} {r : α → α → Prop} (H : WellFounded r) (s : Set α) (h : s.Nonempty) {x : α},
x ∈ s → ¬r x (H.min s h)
The theorem `WellFounded.not_lt_min` states that for any type `α`, a binary relation `r` on `α`, and any nonempty set `s` of `α`, it is not possible for any element `x` in `s` to be less than the minimum element of `s` according to the well-founded relation `r`. In other words, no element in the set `s` can be less than the minimum element of `s` under the ordering defined by `r`.
More concisely: For any type `α`, binary relation `r` on `α`, and nonempty `s ∈ α`, there is no `x ∈ s` such that `x < min s` according to the well-founded relation `r`.
|
Function.argminOn_mem
theorem Function.argminOn_mem :
∀ {α : Type u_1} {β : Type u_2} (f : α → β) [inst : LT β] (h : WellFounded fun x x_1 => x < x_1) (s : Set α)
(hs : s.Nonempty), Function.argminOn f h s hs ∈ s
The theorem `Function.argminOn_mem` states that for any types `α` and `β`, given a function `f` from `α` to `β`, a well-founded less-than relation on `β`, and a non-empty set `s` of `α`, the element of `s`, which is obtained by applying the function `Function.argminOn` to `f`, the well-founded relation, `s`, and the non-emptiness of `s`, is an element of the set `s`. In other words, it guarantees that the `Function.argminOn` function always returns an element from the provided non-empty set `s`, where this element has the minimum image under the function `f` with respect to the provided less-than relation on `β`.
More concisely: For any function `f` from a non-empty set `s` to a type `β` with a well-founded ordering, the element of `s` with minimum image under `f` with respect to the ordering exists in `s`.
|
Acc.induction_bot'
theorem Acc.induction_bot' :
∀ {α : Sort u_4} {β : Sort u_5} {r : α → α → Prop} {a bot : α},
Acc r a →
∀ {C : β → Prop} {f : α → β}, (∀ (b : α), f b ≠ f bot → C (f b) → ∃ c, r c b ∧ C (f c)) → C (f a) → C (f bot)
The theorem `Acc.induction_bot'` is an induction principle that asserts the following: Given a relation `r` on a type `α`, a function `f` from `α` to `β`, a predicate `C` on `β`, and a particular element `bot` of `α`, if every element `a` that is accessible by `r` satisfies `C (f a)`, and for each `b` such that `f b` is not equal to `f bot` and that `C (f b)` holds, there exists a `c` such that `r c b` holds and `C (f c)` holds, then `C (f bot)` also holds. This principle is used for reasoning about properties that hold for all accessible elements and extends to `bot` under the given conditions.
More concisely: If every accessible element `a` in a type `α` satisfies `C(f(a))` and for each `b` not equal to `f(bot)` with `C(f(b))` holding, there exists a `c` such that `r(c, b)` holds and `C(f(c))` holds, then `C(f(bot))` also holds.
|