Monotone.directed_ge
theorem Monotone.directed_ge :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : IsDirected α fun x x_1 => x ≥ x_1] [inst_2 : Preorder β]
{f : α → β}, Monotone f → Directed (fun x x_1 => x ≥ x_1) f
The theorem `Monotone.directed_ge` states that for all types `α` and `β`, if `α` has a preorder relation and is directed with respect to the greater than or equal to relation, and `β` has a preorder relation, then for any function `f` from `α` to `β`, if `f` is a monotone function, it is also directed with respect to the greater than or equal to relation. In other words, if a function preserves the order from a directed set under a preorder relation, then there exists an element in the image of the function that is above any pair of elements in the image.
More concisely: If `α` is a preordered and directed type, `β` is a preordered type, and `f : α → β` is a monotone function, then `f` is a directed function.
|
IsDirected.directed
theorem IsDirected.directed :
∀ {α : Type u_1} {r : α → α → Prop} [self : IsDirected α r] (a b : α), ∃ c, r a c ∧ r b c
This theorem states that for any type `α` and any binary relation `r` defined on `α`, if this relation is directed (as denoted by the `IsDirected α r` class), then for any two elements `a` and `b` of type `α`, there exists an element `c` such that `r a c` and `r b c` hold. In other words, in a directed relation, for any two elements, there is a common element that is related to both of them.
More concisely: In a directed relation on a type `α`, for any `a` and `b` in `α`, there exists a common element `c` such that `(a, c)` and `(b, c)` are in the relation.
|
exists_le_le
theorem exists_le_le :
∀ {α : Type u} [inst : LE α] [inst_1 : IsDirected α fun x x_1 => x ≥ x_1] (a b : α), ∃ c ≤ a, c ≤ b
This theorem, `exists_le_le`, states that for any type `α` that has a less than or equal to (`LE`) operation and for which there is always a 'direction' (expressed by the `IsDirected` property) such that `x` is greater than or equal to `x_1` (i.e., for any two elements, one of them is greater than or equal to the other), if we take any two elements `a` and `b` of this type, there exists another element `c` which is less than or equal to both `a` and `b`.
More concisely: For any type `α` with a directed `LE` relation, given any `a` and `b` in `α`, there exists an element `c` such that `c LE a` and `c LE b`.
|
Directed.directedOn_range
theorem Directed.directedOn_range :
∀ {α : Type u} {ι : Sort w} {r : α → α → Prop} {f : ι → α}, Directed r f → DirectedOn r (Set.range f)
This theorem states that for any type `α`, any sort `ι`, any binary relation `r` on `α`, and any function `f` from `ι` to `α`, if `f` is directed with respect to `r`, then the range of `f` is a directed set with respect to `r`. In other words, if for any two elements `x` and `y` in the domain of `f`, there exists an element `z` such that `f(x) ≼ f(z)` and `f(y) ≼ f(z)`, then for all pairs of elements `x` and `y` in the range of `f`, there exists an element `z` in the range of `f` such that `x ≼ z` and `y ≼ z` for the relation `r`.
More concisely: If `f` is a function from a directed set `(ι, ≤)` to a type `α` such that the image of every pair of related elements in `ι` is related in `α` (i.e., `f(x) ≤ f(y)` whenever `x ≤ y`), then the image `f"[ι]` is a directed set under the relation `≤`.
|
DirectedOn.directed_val
theorem DirectedOn.directed_val :
∀ {α : Type u} {r : α → α → Prop} {s : Set α}, DirectedOn r s → Directed r Subtype.val
This theorem, named "DirectedOn.directed_val", asserts that for any type `α`, any binary relation `r` on `α`, and any set `s` of type `α`, if `s` is directed under the relation `r` (meaning that for any two elements in `s`, there exists another element in `s` that is related under `r` to both elements), then the underlying set of elements in `s`, extracted using the `Subtype.val` function, is also directed under `r`. This is essentially a re-statement or "alias" of one direction of the theorem `directedOn_iff_directed`.
More concisely: If a subset `s` of a type `α` is directed with respect to a binary relation `r`, then the underlying set of elements in `s`, obtained by applying `Subtype.val`, is also directed with respect to `r`.
|
directedOn_iff_directed
theorem directedOn_iff_directed :
∀ {α : Type u} {r : α → α → Prop} {s : Set α}, DirectedOn r s ↔ Directed r Subtype.val
This theorem establishes a correspondence between the concept of a directed set and a directed-on relation. For any type `α` and a binary relation `r` on `α`, it states that a set `s` is directed under the relation `r` (meaning, for any two elements in the set, there exists a third element in the set that is 'above' both under the relation `r`) if and only if the function `Subtype.val` (which extracts the underlying element from a subtype) is directed (meaning, for any two indices, there exists a third index such that its corresponding value is 'above' both previously mentioned values under the relation `r`). Here, 'above' means 'greater than or equal to' in a general sense, specifically defined by the relation `r`.
More concisely: For any type `α` and a binary relation `r` on `α`, a set `s` is directed under `r` if and only if the indices in the subtype of `s` under `r` are directed under `r`.
|
directedOn_of_sup_mem
theorem directedOn_of_sup_mem :
∀ {α : Type u} [inst : SemilatticeSup α] {S : Set α},
(∀ ⦃i j : α⦄, i ∈ S → j ∈ S → i ⊔ j ∈ S) → DirectedOn (fun x x_1 => x ≤ x_1) S
This theorem states that for any type `α` that has a `SemilatticeSup` instance (meaning that it has a supremum operation defined), any set `S` of elements of this type is directed under the `≤` relation if and only if the supremum of any pair of elements in `S` is also in `S`. In other words, if the set `S` is closed under taking supremum, then for any pair of elements in `S`, there exists an element in `S` that is greater than or equal to both of the elements in the pair.
More concisely: For any type `α` with a `SemilatticeSup` instance, a set `S` of `α` is directed if and only if it is closed under taking suprema.
|
directed_of_isDirected_ge
theorem directed_of_isDirected_ge :
∀ {α : Type u} {β : Type v} [inst : LE α] [inst_1 : IsDirected α fun x x_1 => x ≥ x_1] {r : β → β → Prop}
{f : α → β}, (∀ (a₁ a₂ : α), a₁ ≤ a₂ → r (f a₂) (f a₁)) → Directed r f
The theorem `directed_of_isDirected_ge` states that for any types `α` and `β`, given an order (`LE`) on `α` and assuming `α` is downward-directed (meaning for any two elements there exists another element that is greater than or equal to them), along with a relation `r` on `β` and a function `f` from `α` to `β` which is antitone (its values decrease or stay the same as its inputs increase), then the function `f` is directed with respect to the relation `r`. In other words, for any two inputs of `f`, there exists another input such that its value under `f` is related by `r` to the values of the original pair.
More concisely: If `α` is downward-directed, `LE` being the order on `α`, `r` is a relation on `β`, and `f` is an antitone function from `α` to `β`, then `f` is a directed function with respect to `r`.
|
directed_comp
theorem directed_comp :
∀ {α : Type u} {β : Type v} {r : α → α → Prop} {ι : Sort u_1} {f : ι → β} {g : β → α},
Directed r (g ∘ f) ↔ Directed (g ⁻¹'o r) f
The theorem `directed_comp` states that for any types `α`, `β`, and `ι`, a relation `r` on `α`, and functions `f : ι → β` and `g : β → α`, a family of elements is directed by `r` after being transformed by `g ∘ f` if and only if it is directed by the relation `g ⁻¹'o r` before being transformed by `f`. Here, `g ⁻¹'o r` is the preimage of the relation `r` under `g`, which means we apply `g` to the elements before comparing them with `r`. This theorem links the concept of directional relations and function composition.
More concisely: Given types α, β, and ι, a relation r on α, and functions f : ι → β and g : β → α, the families {x\_i : α} are directed by r after being transformed by g ∘ f if and only if they are directed by g ⁻¹'o r before being transformed.
|
exists_ge_ge
theorem exists_ge_ge :
∀ {α : Type u} [inst : LE α] [inst_1 : IsDirected α fun x x_1 => x ≤ x_1] (a b : α), ∃ c, a ≤ c ∧ b ≤ c
This theorem, `exists_ge_ge`, states that for any type `α` that has a less-than-or-equal-to (`≤`) operation and for which a direction can be determined (i.e., it can be decided whether one element is less than or equal to another), given any two elements `a` and `b` of `α`, there exists a third element `c` such that both `a` and `b` are less than or equal to `c`. In mathematical terms, this can be expressed as `∀a, b ∈ α, ∃c ∈ α, a ≤ c ∧ b ≤ c`. This theorem embodies one of the properties of directed sets in order theory.
More concisely: For any type `α` with a decidable `≤` relation, there exists an element `c` such that `a ≤ c` and `b ≤ c` for all `a, b ∈ α`.
|
Antitone.directed_ge
theorem Antitone.directed_ge :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : IsDirected α fun x x_1 => x ≤ x_1] [inst_2 : Preorder β]
{f : α → β}, Antitone f → Directed (fun x x_1 => x ≥ x_1) f
The theorem `Antitone.directed_ge` states that for any types `α` and `β` with preorder relations and a function `f` from `α` to `β`, if `α` is directed with respect to the less than or equal to relation and the function `f` is antitone (meaning that `a ≤ b` implies `f(b) ≤ f(a)`), then the function `f` is directed with respect to the greater than or equal to relation. In other words, for any two elements in the domain of `f`, there exists a third element such that `f` applied to this third element is greater than or equal to `f` applied to each of the original two elements.
More concisely: If `α` is a directed type with respect to `≤`, and `f: α → β` is an antitone function, then `f` is directed with respect to the `≥` relation on `β`.
|
directed_of
theorem directed_of : ∀ {α : Type u} (r : α → α → Prop) [inst : IsDirected α r] (a b : α), ∃ c, r a c ∧ r b c := by
sorry
This theorem states that for any type `α` and a binary relation `r` on `α`, if `α` with `r` is directed (which means that for every pair of elements in `α`, there exists a third element in `α` that is related to both of them), then for any two elements `a` and `b` in `α`, there exists a third element `c` in `α` such that `a` is related to `c` and `b` is related to `c` via the relation `r`.
More concisely: If `α` is a type with a directed binary relation `r`, then for any `a, b ∈ α`, there exists `c ∈ α` such that `r a c` and `r b c`.
|
directedOn_of_inf_mem
theorem directedOn_of_inf_mem :
∀ {α : Type u} [inst : SemilatticeInf α] {S : Set α},
(∀ ⦃i j : α⦄, i ∈ S → j ∈ S → i ⊓ j ∈ S) → DirectedOn (fun x x_1 => x ≥ x_1) S
The theorem `directedOn_of_inf_mem` states that for any type `α` with a structure of `SemilatticeInf` (a semilattice with an infimum operation) and a set `S` of elements of type `α`, if for any two elements `i` and `j` in the set `S`, their infimum `i ⊓ j` is also in `S`, then the set `S` is directed with respect to the relation `≥` (greater than or equal to). In other words, for any two elements in the set, there exists a third element in the set that is greater than or equal to both of them. This theorem connects the property of being stable under infimum operation with the concept of directed sets.
More concisely: If a semilattice `α` with infimum operation has a subset `S` such that for all `i, j ∈ S`, their infimum `i ⊓ j` is in `S`, then `S` is a directed set.
|
isTop_iff_isMax
theorem isTop_iff_isMax :
∀ {α : Type u} [inst : Preorder α] {a : α} [inst_1 : IsDirected α fun x x_1 => x ≤ x_1], IsTop a ↔ IsMax a := by
sorry
This theorem states that for any type `α` with a preorder relation and which also has the property that for any two elements `x` and `x_1`, `x` is less than or equal to `x_1`, an element `a` of `α` is a top element if and only if it is a maximal element. In mathematical terms, for a set `α` with a preorder, an element `a` is considered a top element (i.e., all other elements of the set are less than or equal to `a`) if and only if `a` is a maximal element (i.e., there's no other element in the set that's strictly greater than `a`).
More concisely: A preorder type `α` element `a` is a top element if and only if it is a maximal element.
|
Monotone.directed_le
theorem Monotone.directed_le :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : IsDirected α fun x x_1 => x ≤ x_1] [inst_2 : Preorder β]
{f : α → β}, Monotone f → Directed (fun x x_1 => x ≤ x_1) f
The theorem `Monotone.directed_le` states that for any type `α` and `β` with a preorder structure, and a function `f` from `α` to `β`, if `α` is directed with respect to the relation "less than or equal to" and the function `f` is monotone (meaning that `a ≤ b` implies `f a ≤ f b`), then the image of `α` under `f` is also directed with respect to the relation "less than or equal to". In other words, for any two elements in the image of `α`, there exists a third element that is greater than or equal to both of them.
More concisely: If `α` is a directed type with respect to "≤" and `f: α → β` is a monotone function, then `f["α"]` is a directed set with respect to "≤".
|
directed_of_isDirected_le
theorem directed_of_isDirected_le :
∀ {α : Type u} {β : Type v} [inst : LE α] [inst_1 : IsDirected α fun x x_1 => x ≤ x_1] {f : α → β}
{r : β → β → Prop}, (∀ ⦃i j : α⦄, i ≤ j → r (f i) (f j)) → Directed r f
The theorem `directed_of_isDirected_le` states that for any types `α` and `β`, given `α` has a `≤` relation that makes it upwards-directed, and a monotone function `f` from `α` to `β`, and a relation `r` on `β`, if it holds that for any `i` and `j` in `α` where `i ≤ j` it implies that `r(f(i), f(j))`, then the function `f` is directed with respect to the relation `r`. In other words, given any pair `x` and `y` in the domain of `f`, there is an element `z` such that both `f(x)` and `f(y)` are related to `f(z)` under the relation `r`.
More concisely: If `α` is upwards-directed with respect to `≤`, and `f: α → β` is a monotone function such that `r(f(i), f(j))` holds for all `i ≤ j` in `α`, then `f` is a directed function with respect to `r`.
|
Directed.mono_comp
theorem Directed.mono_comp :
∀ {α : Type u} {β : Type v} (r : α → α → Prop) {ι : Sort u_1} {rb : β → β → Prop} {g : α → β} {f : ι → α},
(∀ ⦃x y : α⦄, r x y → rb (g x) (g y)) → Directed r f → Directed rb (g ∘ f)
The theorem `Directed.mono_comp` states that for any types `α`, `β` and `ι`, a relation `r` on `α`, a relation `rb` on `β`, a function `g` from `α` to `β` and a function `f` from `ι` to `α`, if `g` is monotone with respect to `r` and `rb` (i.e., for any `x` and `y` in `α`, `r x y` implies `rb (g x) (g y)`), and if the function `f` is directed with respect to the relation `r`, then the composed function `g ∘ f` is directed with respect to the relation `rb`. In other words, the directedness property is preserved under the composition of a monotone function.
More concisely: If `g` is a monotone function with respect to `r` and `rb`, and `f` is a function that respects the direction of `r`, then `g ∘ f` is a directed function with respect to `rb`.
|
directed_id
theorem directed_id : ∀ {α : Type u} {r : α → α → Prop} [inst : IsDirected α r], Directed r id
This theorem states that for any given type `α` and a relation `r` on `α` such that `α` is directed with respect to `r`, the identity function `id` is also directed with respect to the same relation `r`. In other words, given any two elements in the range of the identity function, there exists a third element that is related (under `r`) to both of them.
More concisely: If `α` is a directed type and `r` is a relation on `α` such that `α` is directed with respect to `r`, then the identity function `id` on `α` is also a directed function with respect to `r`.
|