Fintype.exists_ge
theorem Fintype.exists_ge :
∀ {α : Type u_1} {β : Type u_2} [inst : Finite β] [inst : Nonempty α] [inst : Preorder α]
[inst_1 : IsDirected α fun x x_1 => x ≥ x_1] (f : β → α), ∃ M, ∀ (i : β), M ≤ f i
The theorem `Fintype.exists_ge` states that for any function `f` from a finite type `β` to a type `α`, where `α` is non-empty and has a preorder (a binary relation that is reflexive and transitive), and such that for any two elements of `α`, there exists an element that is greater than or equal to both, there exists an element `M` in `α` such that `M` is less than or equal to `f i` for all `i` in `β`. In other words, this theorem guarantees the existence of a lower bound `M` for the range of the function `f`.
More concisely: Given a finite type `β` and a function `f` from `β` to a non-empty preordered type `α` with the property that for all `x, y` in `α`, there exists a `z` in `α` such that `x ≤ z` and `y ≤ z`, there exists an element `M` in `α` that is less than or equal to `f(i)` for all `i` in `β`.
|
Directed.fintype_le
theorem Directed.fintype_le :
∀ {α : Type u_1} {r : α → α → Prop} [inst : IsTrans α r] {β : Type u_2} {γ : Type u_3} [inst : Nonempty γ]
{f : γ → α} [inst : Finite β], Directed r f → ∀ (g : β → γ), ∃ z, ∀ (i : β), r (f (g i)) (f z)
This theorem states that given a type `α` and a transitive relation `r` on `α`, types `β` and `γ`, and a non-empty type `γ`, a function `f` from `γ` to `α`, and a function `g` from `β` to `γ`, if the function `f` is directed (i.e., for any two elements of `γ`, there exists a third element that is related to both by `r` through the function `f`), then there exists an element in `γ` such that for every element in `β`, the value of the function `f` at that element under function `g` is related through `r` to the value of `f` at the aforementioned element in `γ`. In other words, this theorem provides a way to find an upper bound in the image of the directed function `f` for any finite set of elements in `β`.
More concisely: Given a transitive relation `r` on a type `α`, a function `f` from a non-empty `γ` to `α`, and functions `g` from `β` to `γ` and `h` from `γ` to `α` such that `h ∘ g = f`, if `f` is directed, then there exists an element in `γ` that is an upper bound for `h` restricted to any finite subset of `β`.
|
Finite.bddAbove_range
theorem Finite.bddAbove_range :
∀ {α : Type u_1} {β : Type u_2} [inst : Finite β] [inst : Nonempty α] [inst : Preorder α]
[inst_1 : IsDirected α fun x x_1 => x ≤ x_1] (f : β → α), BddAbove (Set.range f)
The theorem `Finite.bddAbove_range` states that for any two types `α` and `β` with `α` being a nonempty type with a preorder (a binary relation that is reflexive and transitive) and being directed (any two elements in `α` have an upper bound), and `β` being finite, for any function `f` from `β` to `α`, the range of `f` (the set of all possible outputs of `f`) is bounded above. In other words, there exists an element in `α` that is greater than or equal to every element in the range of `f`.
More concisely: For any nonempty type `α` with a preorder and directed structure, and any finite type `β`, if `f` is a function from `β` to `α`, then the range of `f` has an upper bound in `α`.
|
Finite.exists_le
theorem Finite.exists_le :
∀ {α : Type u_1} {β : Type u_2} [inst : Finite β] [inst : Nonempty α] [inst : Preorder α]
[inst_1 : IsDirected α fun x x_1 => x ≤ x_1] (f : β → α), ∃ M, ∀ (i : β), f i ≤ M
This theorem states that for all types `α` and `β`, given that `β` is finite, `α` is nonempty, and `α` has a preorder structure, and there exists a function `f` from `β` to `α` such that `α` is directed with respect to the preorder (meaning, for any two elements in `α`, there exists a third element that is greater than or equal to both), then there exists an element `M` in `α` such that for all elements `i` in `β`, `f(i)` is less than or equal to `M`. In other words, there is an upper bound `M` in `α` for the image of `f`.
More concisely: If `α` is a nonempty type with a preorder, `β` is finite, and there exists a function `f` from `β` to `α` such that `α` is directed with respect to the preorder, then there exists an upper bound `M` in `α` for the image of `f`.
|
Directed.finite_set_le
theorem Directed.finite_set_le :
∀ {α : Type u_1} {r : α → α → Prop} [inst : IsTrans α r] {γ : Type u_3} [inst : Nonempty γ] {f : γ → α},
Directed r f → ∀ {s : Set γ}, s.Finite → ∃ z, ∀ i ∈ s, r (f i) (f z)
The theorem `Directed.finite_set_le` states that for any type `α` with a transitive relation `r`, and any type `γ` which is nonempty, along with a function `f` mapping elements of `γ` to `α`, if the function `f` is directed with respect to `r`, then for any finite set `s` of elements from `γ`, there exists an element `z` such that for all elements `i` in the set `s`, `r (f i) (f z)` holds, meaning `f z` is `r`-above every element `f i` where `i` is in the set `s`. This essentially says that in a directed family over a finite set, there exists an element that is above all elements in the relation `r`.
More concisely: Given a type `α` with a transitive relation `r`, a nonempty type `γ` and a function `f` mapping `γ` to `α` that is directed with respect to `r`, for any finite set `s` of elements from `γ`, there exists an element `z` in `γ` such that `r (f i) (f z)` holds for all `i` in `s`.
|
Fintype.bddAbove_range
theorem Fintype.bddAbove_range :
∀ {α : Type u_1} {β : Type u_2} [inst : Finite β] [inst : Nonempty α] [inst : Preorder α]
[inst_1 : IsDirected α fun x x_1 => x ≤ x_1] (f : β → α), BddAbove (Set.range f)
This theorem, referred to as `Fintype.bddAbove_range`, states that for any types `α` and `β`, given that `β` is finite and `α` is nonempty and preordered, and there exists a direction in `α` such that for any two elements `x` and `x_1` in `α`, `x` is less than or equal to `x_1`, then for any function `f` from `β` to `α`, the range of `f` is bounded above. In simpler terms, it states that the range of a function from a finite set to a set with an order relation is always bounded above.
More concisely: If `β` is finite and `α` is nonempty and preordered with a bound in `α`, then the range of any function from `β` to `α` is bounded above.
|
Directed.finite_le
theorem Directed.finite_le :
∀ {α : Type u_1} {r : α → α → Prop} [inst : IsTrans α r] {β : Type u_2} {γ : Type u_3} [inst : Nonempty γ]
{f : γ → α} [inst : Finite β], Directed r f → ∀ (g : β → γ), ∃ z, ∀ (i : β), r (f (g i)) (f z)
This theorem states that for any types `α`, `β`, and `γ`, and a relation `r` on `α` that is transitive, if `γ` is nonempty and `β` is finite, and if there is a function `f : γ → α` such that for every pair of elements in `γ`, there exists an element in `γ` larger than both of them with respect to `r`, then for any function `g : β → γ`, there exists an element `z` in `γ` such that for all elements `i` in `β`, `f(g(i))` is less than or equal to `f(z)` with respect to `r`. In simpler terms, this theorem states that for every element in the finite set `β`, there exists a "upper bound" in `γ` with respect to the relation `r`.
More concisely: Given types `α`, `β`, and `γ`, a transitive relation `r` on `α`, a nonempty and finite set `β`, and a function `f : γ → α` such that for every pair of elements in `γ`, there exists an element in `γ` larger than both with respect to `r`, then for every function `g : β → γ`, there exists an element `z` in `γ` such that for all `i` in `β`, `f(g(i)) ≤ f(z)` holds in `α` with respect to `r`.
|
Fintype.exists_le
theorem Fintype.exists_le :
∀ {α : Type u_1} {β : Type u_2} [inst : Finite β] [inst : Nonempty α] [inst : Preorder α]
[inst_1 : IsDirected α fun x x_1 => x ≤ x_1] (f : β → α), ∃ M, ∀ (i : β), f i ≤ M
This theorem, named `Fintype.exists_le`, asserts that given a type `β` that is finite, a nonempty type `α` with a preorder relation, and a function `f` from `β` to `α`, there exists an element `M` in `α` such that for every element `i` in `β`, the value `f(i)` is less than or equal to `M`. In essence, this theorem is stating that for any function mapping from a finite set to a preordered set, there exists an upper bound in the codomain for the image of the function.
More concisely: Given a finite nonempty type `β` with a preorder relation and a function `f` from `β` to a preordered type `α`, there exists an element `M` in `α` such that for all `i` in `β`, `f(i) ≤ M`.
|
Fintype.bddBelow_range
theorem Fintype.bddBelow_range :
∀ {α : Type u_1} {β : Type u_2} [inst : Finite β] [inst : Nonempty α] [inst : Preorder α]
[inst_1 : IsDirected α fun x x_1 => x ≥ x_1] (f : β → α), BddBelow (Set.range f)
The theorem `Fintype.bddBelow_range` states that for any type `α` that has an order relation and for any finite type `β`, if `α` is nonempty and directed towards greater elements, then for any function `f` from `β` to `α`, the set of all image points of `f` (the range of `f`) has a lower bound. In other words, there exists some element in `α` such that it is less than or equal to every element in the range of `f`.
More concisely: For any nonempty, directed type `α` with an order relation and any finite type `β`, if `α` maps to `α` by any function `f` from `β`, then the range of `f` has a least element in `α`.
|