maximals_subset
theorem maximals_subset : ∀ {α : Type u_1} (r : α → α → Prop) (s : Set α), maximals r s ⊆ s
The theorem `maximals_subset` states that for any type `α`, any binary relation `r` on `α`, and any set `s` of type `α`, the set of maximal elements in `s` (with respect to `r`) is a subset of `s`. Here, a maximal element of `s` is an element `a` in `s` such that for any other element `b` in `s`, if `r` holds between `a` and `b`, then `r` also holds between `b` and `a`.
More concisely: For any type `α`, relation `r` on `α`, and set `s` of `α`, the set of maximal elements in `s` (with respect to `r`) is a subset of `s`. (A maximal element `a` in `s` is an element such that for all `b` in `s`, if `a` `r` `b`, then `b` `r` `a`.)
|
OrderIso.map_mem_maximals
theorem OrderIso.map_mem_maximals :
∀ {β : Type u_2} {α : Type u_1} [inst : LE α] [inst_1 : LE β] {s : Set α} {t : Set β} (f : ↑s ≃o ↑t) {x : α}
(hx : x ∈ maximals (fun x x_1 => x ≤ x_1) s), ↑(f ⟨x, ⋯⟩) ∈ maximals (fun x x_1 => x ≤ x_1) t
The theorem `OrderIso.map_mem_maximals` states that for any two types `α` and `β` with a less than or equal to (`<=`) order defined on them, given a set `s` of type `α` and a set `t` of type `β`, if there exists an order-isomorphism `f` between the sets `s` and `t`, then for any element `x` in the maximal elements of set `s` (where the maximal elements are defined with respect to the `<=` order), the image of `x` under the isomorphism `f` is in the maximal elements of set `t` (also defined with respect to the `<=` order). Essentially, the order isomorphism preserves the property of being a maximal element.
More concisely: If `f` is an order isomorphism between sets `s` and `t` with respect to a given order `<=`, then for any maximal element `x` in `s`, `f(x)` is a maximal element in `t`.
|
image_minimals_of_rel_iff_rel
theorem image_minimals_of_rel_iff_rel :
∀ {β : Type u_2} {α : Type u_1} {f : α → β} {r : α → α → Prop} {s : β → β → Prop} {x : Set α},
(∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))) → f '' minimals r x = minimals s (f '' x)
The theorem `image_minimals_of_rel_iff_rel` states that for any types `α` and `β`, a function `f` from `α` to `β`, a binary relation `r` on `α`, a binary relation `s` on `β`, and a set `x` of type `α`, if for every pair of elements `a` and `a'` in `x` the relation `r` holds between `a` and `a'` if and only if the relation `s` holds between `f(a)` and `f(a')`, then the image of the set of minimal elements under `r` in `x` under the function `f` is equal to the set of minimal elements under `s` in the image of `x` under `f`. In other words, if `f` preserves the relation between elements of `x`, it also preserves the set of minimal elements under these relations when applied to `x`.
More concisely: If a function preserves the relation between elements of a set such that two elements are related if and only if their images under the function are related, then the images under the function of the minimal elements of the set are the minimal elements of the image set.
|
map_mem_minimals
theorem map_mem_minimals :
∀ {β : Type u_2} {α : Type u_1} {f : α → β} {r : α → α → Prop} {s : β → β → Prop} {x : Set α},
(∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))) →
∀ {a : α}, a ∈ minimals r x → f a ∈ minimals s (f '' x)
The theorem `map_mem_minimals` is a statement about the transformation of antichains. It states that for any two types `α` and `β`, a function `f` from `α` to `β`, a relation `r` on `α`, a relation `s` on `β`, and a set `x` of type `α`, if for all `a` and `a'` in `x`, `a` relates to `a'` under `r` if and only if `f(a)` relates to `f(a')` under `s`, then for any `a` in the set of minimal elements of `x` under `r`, `f(a)` is in the set of minimal elements of the image of `x` under `f` with respect to `s`.
In simpler terms, this theorem says if you have a function that preserves the relationship of elements when mapping from one set to another, then the image of any minimal element in the original set under the function is a minimal element in the image set.
More concisely: If a function preserves the relation between minimal elements of two sets, then the image of any minimal element under the function is a minimal element in the image set.
|
mem_minimals_iff_forall_lt_not_mem'
theorem mem_minimals_iff_forall_lt_not_mem' :
∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {x : α} (rlt : α → α → Prop)
[inst : IsNonstrictStrictOrder α r rlt], x ∈ minimals r s ↔ x ∈ s ∧ ∀ ⦃y : α⦄, rlt y x → y ∉ s
This theorem asserts that for any type `α`, a relation `r`, a set `s` of type `α`, and an element `x` of type `α`, given a secondary relation (denoted as `rlt`), if the relation `r` along with `rlt` forms a nonstrict-strict order on `α`, then `x` belongs to the set of minimal elements of `s` with respect to `r` if and only if `x` belongs to `s` and for every element `y` of type `α`, if `y` is strictly less than `x` with respect to `rlt`, then `y` does not belong to `s`. The theorem specifies that it can't be used for rewriting without specifying `rlt`. The theorem has versions for the subset (`⊆`) and less than or equal to (`≤`) relations as well.
More concisely: Given a type `α`, a relation `r`, a set `s`, and an element `x` of type `α`, if `r` and a secondary relation `rlt` form a nonstrict-strict order on `α`, then `x` is a minimal element of `s` with respect to `r` if and only if `x` is in `s` and no strictly smaller elements of `s` with respect to `rlt` exist.
|
OrderIso.map_mem_minimals
theorem OrderIso.map_mem_minimals :
∀ {β : Type u_2} {α : Type u_1} [inst : LE α] [inst_1 : LE β] {s : Set α} {t : Set β} (f : ↑s ≃o ↑t) {x : α}
(hx : x ∈ minimals (fun x x_1 => x ≤ x_1) s), ↑(f ⟨x, ⋯⟩) ∈ minimals (fun x x_1 => x ≤ x_1) t
The theorem `OrderIso.map_mem_minimals` states that for any two types `α` and `β` with preorder relations, and any two sets `s` of type `α` and `t` of type `β`, if there exists an order isomorphism `f` from `s` to `t`, then for any element `x` in `s` that belongs to the minimal elements of `s` under the order relation `≤`, the image of `x` under `f` belongs to the minimal elements of `t` under the same order relation. Here, the minimal elements of a set are those for which there are no other elements in the set that are strictly less than them.
More concisely: If `f` is an order isomorphism from a set `s` with minimal elements `x` under relation `≤` to a set `t`, then the image `f(x)` is a minimal element in `t` under the same relation `≤`.
|
IsAntichain.max_maximals
theorem IsAntichain.max_maximals :
∀ {α : Type u_1} {r : α → α → Prop} {s t : Set α},
IsAntichain r t → maximals r s ⊆ t → (∀ ⦃a : α⦄, a ∈ t → ∃ b ∈ maximals r s, r b a) → maximals r s = t
This theorem states that for any type `α`, relation `r`, and sets `s` and `t` of `α`, if `t` forms an antichain under the relation `r`, and if set `s` turned into an antichain (`maximals r s`) is a subset of `t` that 'shadows' `t` (meaning that each element `a` of `t` has some `b` in `maximals r s` where `b` is related to `a` under `r`), then `maximals r s` is actually equal to `t`. This theorem captures an interesting property of antichains and maximal elements under a relation in a set.
More concisely: If `t` is an antichain of a relation `r` on a type `α` and `s` is another set such that `maximals r s` is a subset of `t` that shadows `t`, then `maximals r s` equals `t`.
|
eq_of_mem_maximals
theorem eq_of_mem_maximals :
∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {a b : α} [inst : IsAntisymm α r],
a ∈ maximals r s → b ∈ s → r a b → a = b
This theorem states that for any type `α`, any binary relation `r` on `α`, any set `s` of type `α`, and any two elements `a` and `b` of type `α`, if the binary relation `r` is antisymmetric and `a` is a maximal element of `s` under the relation `r`, then if `b` is in `s` and `a` is related to `b` by `r`, it must be that `a` equals `b`. In other words, if `a` is a maximal element of `s` and `r` relates `a` to `b` where `b` is in `s`, there can't be any element `b` that is strictly greater than `a` under `r`, confirming the antisymmetry of `r`.
More concisely: If a binary relation is antisymmetric and an element is a maximal element under the relation in a set, then it is equal to any other element related to it by the relation in the set.
|
eq_of_mem_minimals
theorem eq_of_mem_minimals :
∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {a b : α} [inst : IsAntisymm α r],
a ∈ minimals r s → b ∈ s → r b a → a = b
The theorem `eq_of_mem_minimals` states that for any type `α`, any relation `r` on `α`, any set `s` of type `α`, and any two elements `a` and `b` of type `α`, if `r` is an antisymmetric relation, `a` belongs to the set of minimal elements of `s` with respect to `r`, `b` belongs to `s`, and `r` holds between `b` and `a`, then `a` must be equal to `b`. In essence, this theorem captures the idea that if `a` is a minimal element and `b` is any element such that `b` is related to `a` by `r`, then `a` and `b` must be the same element, highlighting the unique characteristic of the minimal elements in an antisymmetric relation.
More concisely: If `r` is an antisymmetric relation on `α`, `a` is a minimal element of `s` with respect to `r`, `b` is in `s`, and `r(a, b)` holds, then `a = b`.
|
inter_minimals_preimage_inter_eq_of_rel_iff_rel_on
theorem inter_minimals_preimage_inter_eq_of_rel_iff_rel_on :
∀ {β : Type u_2} {α : Type u_1} {f : α → β} {r : α → α → Prop} {s : β → β → Prop} {x : Set α},
(∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))) →
∀ (y : Set β), x ∩ f ⁻¹' minimals s (f '' x ∩ y) = minimals r (x ∩ f ⁻¹' y)
The theorem `inter_minimals_preimage_inter_eq_of_rel_iff_rel_on` states the following:
Given two types, `α` and `β`, a function `f` from `α` to `β`, a relation `r` on `α`, a relation `s` on `β`, and a set `x` of `α`, if for all pairs `a` and `a'` in `x`, the relation `r` holds between `a` and `a'` if and only if the relation `s` holds between `f(a)` and `f(a')`, then for any set `y` of `β`, the intersection of `x` and the preimage under `f` of the minimal elements of the intersection of the image of `x` under `f` and `y` with respect to `s`, is equal to the set of minimal elements of the intersection of `x` and the preimage of `y` under `f` with respect to `r`.
In other words, this theorem relates the minimal elements of a preimage under a function with the minimal elements of the original set, given a particular relationship between the function and the relational structure on the domain and codomain.
More concisely: If for all pairs of elements in a set x, the relation r holds between them if and only if s holds between their images under f, then the minimal elements of the intersection of x and the preimage of a set y under f with respect to r are equal to the minimal elements of the intersection of x and the image of y under f with respect to s.
|
IsAntichain.max_minimals
theorem IsAntichain.max_minimals :
∀ {α : Type u_1} {r : α → α → Prop} {s t : Set α},
IsAntichain r t → minimals r s ⊆ t → (∀ ⦃a : α⦄, a ∈ t → ∃ b ∈ minimals r s, r a b) → minimals r s = t
This theorem states that for any type `α` and any relation `r` on `α`, and for any sets `s` and `t` of type `α`, if `t` is an antichain (a set where no two distinct elements are related by `r`) and the set of minimal elements in `s` (those elements `a` in `s` for which there is no `b` in `s` such that `b` is related by `r` to `a` but not vice versa) is a subset of `t`, and furthermore every element of `t` is related by `r` to some element in the set of minimal elements in `s`, then the set of minimal elements in `s` is exactly equal to `t`. This theorem is about the interplay between the concepts of minimal elements, antichains and the relation between elements in different sets.
More concisely: If `s` is a set of minimal elements of `α` that is an antichain and every element in an antichain `t` of `α` is related to some element in `s`, then `s = t`.
|