Set.PairwiseDisjoint.subset
theorem Set.PairwiseDisjoint.subset :
∀ {α : Type u_1} {ι : Type u_4} [inst : PartialOrder α] [inst_1 : OrderBot α] {s t : Set ι} {f : ι → α},
t.PairwiseDisjoint f → s ⊆ t → s.PairwiseDisjoint f
The theorem `Set.PairwiseDisjoint.subset` states that for any types `α` and `ι`, with `α` being a partially ordered set that also has a least element, if a set `t` of elements of type `ι` is pairwise disjoint under a function `f` from `ι` to `α`, then any subset `s` of `t` is also pairwise disjoint under the same function `f`. In other words, if the images of any two different elements of `t` under `f` do not overlap, this will also hold for any subset `s` of `t`.
More concisely: If `α` is a partially ordered set with a least element and `f : ι → α` is a function such that the images of distinct elements in any pairwise disjoint set `t` of `ι` under `f` are disjoint, then any subset `s` of `t` is also pairwise disjoint under `f`.
|
Set.pairwise_singleton
theorem Set.pairwise_singleton : ∀ {α : Type u_1} (a : α) (r : α → α → Prop), {a}.Pairwise r
The theorem `Set.pairwise_singleton` states that for any type `α`, any element `a` of type `α`, and any binary relation `r` defined on `α`, the relation `r` holds pairwise on the singleton set `{a}`. In more detail, this means that for all distinct elements `x` and `y` from the singleton set `{a}`, `r x y` is true. However, since a singleton set has only one element, there are no distinct elements, so the condition is trivially satisfied.
More concisely: For any type `α`, any element `a` of type `α`, and any binary relation `r` on `α`, `r` holds between every pair of distinct elements in the singleton set `{a}`. (However, since a singleton set has only one element, this condition is vacuously satisfied.)
|
Mathlib.Data.Set.Pairwise.Basic._auxLemma.2
theorem Mathlib.Data.Set.Pairwise.Basic._auxLemma.2 :
∀ {α : Type u_1} (a : α) (r : α → α → Prop), {a}.Pairwise r = True
The theorem states that for any type `α`, any element `a` of type `α`, and any relation `r` between elements of type `α`, the relation `r` holds pairwise on the set that only contains the element `a`. In other words, the relation `r` holds for all distinct pairs of elements in the singleton set `{a}`, which is trivially true since there are no distinct pairs in a singleton set.
More concisely: For any type `α`, relation `r` on `α`, and element `a` in `α`, the singleton set {`a`} satisfies pairwise `r`. That is, `a` `r` `a` and there are no other distinct elements to check.
|
Set.pairwise_insert_of_symmetric
theorem Set.pairwise_insert_of_symmetric :
∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α},
Symmetric r → ((insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, a ≠ b → r a b)
This theorem states that for any type `α`, a binary relation `r` defined on `α`, a set `s` of `α`, and an element `a` of `α`, if the relation `r` is symmetric, then the relation `r` holds pairwise on the set obtained by inserting `a` into `s` if and only if `r` holds pairwise on the set `s` and `r` holds between `a` and any distinct element `b` in `s`. This theorem connects the property of pairwise relations on a set with the concept of symmetric relations. It essentially says that inserting an element into a set preserves the pairwise property of a symmetric relation.
More concisely: For any type `α`, set `s` of `α`, element `a` in `α`, and symmetric binary relation `r` on `α`, `r` holds pairwise on `s ∪ {a}` if and only if `r` holds pairwise on `s` and `r(a, b)` for all distinct `b` in `s`.
|
Set.pairwise_univ
theorem Set.pairwise_univ : ∀ {α : Type u_1} {r : α → α → Prop}, Set.univ.Pairwise r ↔ Pairwise r
The theorem `Set.pairwise_univ` states that, for any type `α` and any relation `r` on `α`, the relation `r` is pairwise on the universal set of `α` if and only if the relation `r` is pairwise on `α`. Here, a relation `r` is said to be pairwise on a set if `r x y` holds for all distinct `x` and `y` in the set, and it is said to be pairwise on a type if `r i j` holds for all distinct `i` and `j` of the type. The universal set of a type `α` is the set containing all elements of `α`.
More concisely: A relation on a type is pairwise with respect to the universal set if and only if it is pairwise on the type itself.
|
Set.pairwise_eq_iff_exists_eq
theorem Set.pairwise_eq_iff_exists_eq :
∀ {α : Type u_1} {ι : Type u_4} [inst : Nonempty ι] (s : Set α) (f : α → ι),
(s.Pairwise fun x y => f x = f y) ↔ ∃ z, ∀ x ∈ s, f x = z
The theorem `Set.pairwise_eq_iff_exists_eq` states that, for any types `α` and `ι` with `ι` being nonempty and a function `f : α → ι`, the function `f` takes pairwise equal values on a set `s` if and only if there exists some `z` in `ι` such that `f` takes the value `z` for each element `x` in `s`. In other words, `f` yields the same value for all elements of `s` if and only if that value `z` exists in the output type `ι`. This theorem has a variant `Set.Nonempty.pairwise_eq_iff_exists_eq` which assumes `s` being nonempty.
More concisely: For any nonempty type `ι` and function `f : α → ι`, the function `f` maps pairwise equal elements of a set `s` to the same value if and only if there exists an element `z` in `ι` such that `f(x) = z` for all `x` in `s`.
|
Mathlib.Data.Set.Pairwise.Basic._auxLemma.6
theorem Mathlib.Data.Set.Pairwise.Basic._auxLemma.6 : ∀ {a : Prop}, (a ∧ a) = a
This theorem states that for all propositions `a`, the conjunction of `a` and `a` (written as `a ∧ a`) is logically equivalent to `a` itself. In other words, if a particular statement `a` is true, then it is redundant to say `a` and `a` is true. Conversely, if `a` and `a` is true, then `a` must be true.
More concisely: For all propositions `a`, `a ∧ a` is logically equivalent to `a`.
|
Set.Pairwise.mono'
theorem Set.Pairwise.mono' : ∀ {α : Type u_1} {r p : α → α → Prop} {s : Set α}, r ≤ p → s.Pairwise r → s.Pairwise p
This theorem states that for any type `α`, two relations `r` and `p` (where a relation is a function from `α` to `α` to `Prop`), and a set `s` of type `α`, if `r` is a sub-relation of `p` (that is, `r` implies `p` for all arguments) and if the relation `r` holds pairwise on set `s` (in other words, for all distinct elements `x` and `y` in `s`, `r x y` holds), then the relation `p` also holds pairwise on the set `s`. This means that imposing a stronger relation does not disrupt the pairwise property for distinct elements in the set.
More concisely: If `r` is a sub-relation of `p` and `r` holds pairwise on set `s`, then `p` also holds pairwise on `s`.
|
Set.pairwiseDisjoint_image_left_iff
theorem Set.pairwiseDisjoint_image_left_iff :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {s : Set α} {t : Set β},
(∀ b ∈ t, Function.Injective fun a => f a b) →
((t.PairwiseDisjoint fun b => (fun a => f a b) '' s) ↔ Set.InjOn (fun p => f p.1 p.2) (s ×ˢ t))
The theorem states that, for any types `α`, `β`, `γ`, a binary function `f : α → β → γ`, and sets `s : Set α` and `t : Set β`, if for all elements `b` in `t` the function `a => f a b` is injective, then the partial images of `f` are pairwise disjoint if and only if `f` is injective on the Cartesian product of `s` and `t`. Here, a function `f : α → β → γ` is considered to have partial images when it is partially evaluated with an argument from `s` to generate a function `β → γ`, and these are pairwise disjoint if their images don't overlap. Function `f` being injective on `s ×ˢ t` means that if `(a₁, b₁), (a₂, b₂) ∈ s ×ˢ t` and `f a₁ b₁ = f a₂ b₂`, then `(a₁, b₁) = (a₂, b₂)`.
More concisely: For any types `α`, `β`, `γ` and sets `s ⊆ α`, `t ⊆ β`, if the restrictions of the binary function `f : α → β → γ` to elements of `t` are injective, then `f` is injective on `s × t` if and only if the partial images of `f` on `s` are pairwise disjoint.
|
Pairwise.set_of_subtype
theorem Pairwise.set_of_subtype :
∀ {α : Type u_1} (s : Set α) (r : α → α → Prop), (Pairwise fun x y => r ↑x ↑y) → s.Pairwise r
The theorem `Pairwise.set_of_subtype` states that for any type `α`, set `s` of type `α`, and relation `r` between elements of type `α`, if `r` holds pairwise for all pairs of elements of the subtype corresponding to `s`, then `r` holds pairwise for all pairs of elements in `s`. In other words, if a relation is pairwise on a subset defined by a certain property, then it is pairwise on the corresponding set.
More concisely: If a relation holds pairwise for all elements in the subtype defined by a property, then it holds pairwise for all elements in the corresponding set.
|
Set.Subsingleton.pairwise
theorem Set.Subsingleton.pairwise : ∀ {α : Type u_1} {s : Set α}, s.Subsingleton → ∀ (r : α → α → Prop), s.Pairwise r
This theorem states that for any set `s` of a certain type `α`, if `s` is a subsingleton (meaning it contains at most one element), then any relation `r` holds pairwise on the set `s`. In other words, for any two distinct elements `x` and `y` in `s`, `r(x, y)` holds true. This is trivially true as there can't be two distinct elements in a subsingleton set.
More concisely: If `s` is a subsingleton set, then for any relation `r` on `s`, `r(x, y)` holds for all distinct elements `x` and `y` in `s`.
|
Set.pairwise_insert_of_symmetric_of_not_mem
theorem Set.pairwise_insert_of_symmetric_of_not_mem :
∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α},
Symmetric r → a ∉ s → ((insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, r a b)
The theorem `Set.pairwise_insert_of_symmetric_of_not_mem` states that for any type `α`, any binary relation `r` on `α`, any set `s` of type `α`, and any element `a` of type `α`, if the relation `r` is symmetric and the element `a` is not in the set `s`, then the property of the relation `r` holding pairwise on the set resulting from the insertion of `a` into `s` is equivalent to the conjunction of the property of the relation `r` holding pairwise on the original set `s` and the property that for all elements `b` in the set `s`, the relation `r` holds between `a` and `b`. In other words, the relation `r` holds pairwise on the set with an extra element `a` (who wasn't originally in the set) if and only if the relation held pairwise on the original set and it also holds between `a` and all elements of the original set, given `r` is symmetric.
More concisely: For any type `α`, binary relation `r` on `α`, set `s` of `α`, and element `a` not in `s`, if `r` is symmetric then `r` holds pairwise between all elements in `s ∪ {a}` if and only if `r` holds pairwise in `s` and `r(a, b)` holds for all `b` in `s`.
|
Mathlib.Data.Set.Pairwise.Basic._auxLemma.17
theorem Mathlib.Data.Set.Pairwise.Basic._auxLemma.17 :
∀ {α : Sort u_1} {p : α → Prop} {a1 a2 : { x // p x }}, (a1 = a2) = (↑a1 = ↑a2)
This theorem states that for any type `α`, any predicate `p` on `α`, and any two elements `a1` and `a2` of the subtype of `α` consisting of elements satisfying `p`, `a1` and `a2` are equal if and only if their underlying elements in `α` are equal. In other words, two elements of a subtype are equal if and only if their representatives in the original type are equal.
More concisely: For any type `α`, predicate `p` on `α`, and elements `a1` and `a2` of the subtype of `α` satisfying `p`, `a1` equals `a2` if and only if their underlying elements in `α` are equal.
|
Set.InjOn.pairwise_image
theorem Set.InjOn.pairwise_image :
∀ {α : Type u_1} {ι : Type u_4} {r : α → α → Prop} {f : ι → α} {s : Set ι},
Set.InjOn f s → ((f '' s).Pairwise r ↔ s.Pairwise (r on f))
This theorem, `Set.InjOn.pairwise_image`, states that for any given types `α` and `ι`, a relation `r` between elements of type `α`, a function `f` from type `ι` to type `α`, and a set `s` of type `ι`: If the function `f` is injective on the set `s`, then the set of images `f '' s` is pairwise related by `r` if and only if the set `s` is pairwise related by the relation `r` composed on function `f`. The pairwise relation indicates that the relation `r` holds for each pair of distinct elements in the set. This theorem essentially relates the pairwise relation on a set and its image under an injective function.
More concisely: For any types `α`, `ι`, relation `r` on `α`, function `f : ι → α`, and set `s ⊆ ι`, if `f` is injective on `s`, then `r` holds between any pair of distinct elements in `s` if and only if it holds between their images under `f`.
|
Set.Pairwise.of_refl
theorem Set.Pairwise.of_refl :
∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} [inst : IsRefl α r],
s.Pairwise r → ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → r a b
This theorem, named `Set.Pairwise.of_refl`, states that for any type `α` and a reflexive relation `r` on `α`, if `r` holds pairwise for all distinct elements in a set `s` of type `α`, then `r` holds for all elements in `s`, not just the distinct ones. In more formal terms, given a set `s` of elements of type `α` and a reflexive relation `r` on `α`, if ∀ `x`, `y` ∈ `s` such that `x` ≠ `y`, `r x y` holds, then ∀ `a`, `b` ∈ `s`, `r a b` also holds. Here, a reflexive relation is one for which every element is related to itself.
More concisely: If a reflexive relation holds pairwise between all distinct elements of a set, then it holds for all elements in the set.
|
Set.Nonempty.pairwise_eq_iff_exists_eq
theorem Set.Nonempty.pairwise_eq_iff_exists_eq :
∀ {α : Type u_1} {ι : Type u_4} {s : Set α},
s.Nonempty → ∀ {f : α → ι}, (s.Pairwise fun x y => f x = f y) ↔ ∃ z, ∀ x ∈ s, f x = z
The theorem `Set.Nonempty.pairwise_eq_iff_exists_eq` states that for a nonempty set `s` of type `α` and a function `f` mapping elements of `α` to some type `ι`, `f` takes pairwise equal values on `s` if and only if there exists some `z` in the codomain `ι` such that `f` maps all elements `x` in `s` to `z`. In other words, if for every pair of distinct elements `x` and `y` in `s`, `f(x)` equals `f(y)`, then there is a specific value `z` in the codomain that `f` maps every element of `s` to, and vice versa.
More concisely: For a nonempty set `s` and a function `f` from `s` to some type `ι`, `f` maps pairwise equal elements of `s` if and only if there exists `z` in `ι` such that `f(x) = z` for all `x` in `s`.
|
Set.injOn_iff_pairwise_ne
theorem Set.injOn_iff_pairwise_ne :
∀ {α : Type u_1} {ι : Type u_4} {f : ι → α} {s : Set ι}, Set.InjOn f s ↔ s.Pairwise fun x x_1 => f x ≠ f x_1 := by
sorry
This theorem states that for any types `α` and `ι`, function `f` from `ι` to `α`, and set `s` of type `ι`, the function `f` is injective on the set `s` if and only if the relation "`f` applied to `x` is not equal to `f` applied to `x_1`" holds pairwise for all distinct elements `x` and `x_1` in `s`. In other words, `f` is injective on `s` precisely when, for every pair of distinct elements in `s`, their images under `f` are also distinct.
More concisely: A function `f` from a set `s` to type `α` is injective if and only if distinct elements in `s` map to distinct images under `f`.
|
Set.pairwise_empty
theorem Set.pairwise_empty : ∀ {α : Type u_1} (r : α → α → Prop), ∅.Pairwise r
The theorem `Set.pairwise_empty` states that for any type `α` and any relation `r` defined on `α`, the relation `r` is pairwise on the empty set. In other words, the property that for any two distinct elements in the set, the relation `r` holds between them, is trivially true for the empty set, because there are no two distinct elements in the empty set.
More concisely: The empty relation is reflexive and pairwise on the empty set. (In the context of Lean's `Set.pairwise_empty` theorem, where the relation `r` is empty, this statement holds.)
|
Set.PairwiseDisjoint.elim
theorem Set.PairwiseDisjoint.elim :
∀ {α : Type u_1} {ι : Type u_4} [inst : PartialOrder α] [inst_1 : OrderBot α] {s : Set ι} {f : ι → α},
s.PairwiseDisjoint f → ∀ {i j : ι}, i ∈ s → j ∈ s → ¬Disjoint (f i) (f j) → i = j
This theorem states that, given a partially ordered type `α` with a bottom element, a set `s` of elements of type `ι`, and a function `f` mapping `ι` to `α`, if `s` is pairwise disjoint under `f`, then for any two elements `i` and `j` in `s`, if the images of `i` and `j` under `f` are not disjoint (i.e., their greatest lower bound is not the bottom element of `α`), then `i` must be equal to `j`. In essence, this theorem ensures the uniqueness of elements in a pairwise disjoint set under a certain function, based on a property of their images under that function in a lattice structure.
More concisely: Given a partially ordered type `α` with a bottom element, if `s` is a pairwise disjoint set of elements of type `ι` and `f : ι → α` is a function, then for any distinct `i, j ∈ s`, if `f i` and `f j` have a greatest lower bound that is not the bottom element of `α`, then `i = j`.
|
Set.Pairwise.subtype
theorem Set.Pairwise.subtype :
∀ {α : Type u_1} (s : Set α) (r : α → α → Prop), s.Pairwise r → Pairwise fun x y => r ↑x ↑y
The theorem `Set.Pairwise.subtype` establishes a connection between the concepts of pairwise property for sets and subtypes in a certain direction. Specifically, it states that for any set `s` of elements of some type `α` and any relation `r` between elements of `α`, if the relation `r` holds pairwise on the set `s` (meaning that `r` is true for all distinct pairs `x, y` in `s`), then the same relation `r` holds pairwise for all distinct elements `x` and `y` when they are viewed as elements of the subtype of `α` induced by `s`. Here, `↑x` and `↑y` denote the elements `x` and `y` viewed as elements of the said subtype.
More concisely: If a relation holds pairwise between all distinct elements of a set, then it also holds pairwise between the same elements viewed as elements of the subtype induced by that set.
|
Set.pairwiseDisjoint_image_right_iff
theorem Set.pairwiseDisjoint_image_right_iff :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {s : Set α} {t : Set β},
(∀ a ∈ s, Function.Injective (f a)) →
((s.PairwiseDisjoint fun a => f a '' t) ↔ Set.InjOn (fun p => f p.1 p.2) (s ×ˢ t))
The theorem states that for any types `α`, `β`, and `γ`, any function `f` from `α` and `β` to `γ`, and any sets `s` and `t` of type `α` and `β` respectively, if the function `f` is injective when partially applied to any element of `s`, then the partial images of `f` with respect to these elements are pairwise disjoint if and only if the function `f` is injective on the Cartesian product of `s` and `t`.
Here, a function `f` is said to be injective when its output uniquely determines its input -- that is, if `f(x) = f(y)` then `x` must be equal to `y`. The term "pairwise disjoint" refers to a collection of sets where no two sets have a common element. And "injective on the Cartesian product of `s` and `t`" means that for any pair of elements `(x1, y1)` and `(x2, y2)` in the Cartesian product of `s` and `t` (which is the set of all possible pairs of elements from `s` and `t`), if `f(x1, y1) = f(x2, y2)` then `(x1, y1)` must be equal to `(x2, y2)`.
More concisely: For any functions `f` from the product of types `α × β` to type `γ`, if `f` is injective on `α × β` if and only if the partial images of `f` on any sets `s ∈ α` and `t ∈ β` are pairwise disjoint.
|
Mathlib.Data.Set.Pairwise.Basic._auxLemma.1
theorem Mathlib.Data.Set.Pairwise.Basic._auxLemma.1 : ∀ {α : Type u_1} (r : α → α → Prop), ∅.Pairwise r = True := by
sorry
This theorem states that for any type `α` and a relation `r` between elements of type `α`, the relation `r` holds pairwise on the empty set. In mathematical terms, this means that for all distinct `x` and `y` in the empty set, `r x y` is true. However, since there are no elements in the empty set, this condition is vacuously true.
More concisely: For any relation `r` on type `α`, `r` holds on the empty set. (Vacuously true)
|
Set.Pairwise.subsingleton
theorem Set.Pairwise.subsingleton : ∀ {α : Type u_1} {s : Set α}, s.Pairwise ⊥ → s.Subsingleton
This theorem, `Set.Pairwise.subsingleton`, states that for any type `α` and any set `s` of type `α`, if the set `s` satisfies the property `Pairwise ⊥` (meaning, for the binary relation `⊥`, which represents the empty relation, every two distinct elements `i` and `j` in the set `s` hold the relation), then `s` is a `Subsingleton`. In other words, if a set holds an empty relation pairwise, it must be a `Subsingleton`, implying that it contains at most one element.
More concisely: If a set is pairwise related to the empty relation, then it is a subsingleton.
|
Set.pairwise_insert
theorem Set.pairwise_insert :
∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α},
(insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, a ≠ b → r a b ∧ r b a
This theorem states that for any type `α`, relation `r` of type `α → α → Prop`, set `s` of type `Set α`, and element `a` of type `α`, the relation `r` holds pairwise on the set resulting from inserting `a` into `s` if and only if the relation `r` holds pairwise on the original set `s` and for every element `b` in `s`, if `a` is not equal to `b`, then the relation `r` holds for both `a` and `b` and vice versa.
More concisely: For any type `α`, set `s` of elements from `α`, and relation `r` on `α`, if `r` holds pairwise on `s ∪ {a}`, where `a` is an element not in `s`, if and only if `r` holds pairwise on `s` and `r` holds for all distinct `a, b` in `s ∪ {a}`, then `r` is an equivalence relation on `s ∪ {a}`.
|
pairwise_disjoint_on_bool
theorem pairwise_disjoint_on_bool :
∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b : α},
Pairwise (Disjoint on fun c => bif c then a else b) ↔ Disjoint a b
This theorem states that for any type `α` that is a semilattice with infimum and has a bottom element, and for any two elements `a` and `b` of type `α`, the pairwise disjointness of a function that maps Boolean values to `a` and `b` (i.e., the function returns `a` for `true` and `b` for `false`) is equivalent to `a` and `b` being disjoint. The function being pairwise disjoint means that for any two different Boolean values, the mapped elements are disjoint, and `a` and `b` being disjoint means that any element of `α` that is less than or equal to both `a` and `b` is also less than or equal to the bottom element of `α`.
More concisely: For any semilattice with infimum and bottom element α, two elements a and b are disjoint if and only if the function mapping true to a and false to b is pairwise disjoint.
|
Set.Pairwise.mono
theorem Set.Pairwise.mono : ∀ {α : Type u_1} {r : α → α → Prop} {s t : Set α}, t ⊆ s → s.Pairwise r → t.Pairwise r := by
sorry
The theorem `Set.Pairwise.mono` states that for any type `α` and any relation `r` defined on `α`, given two sets `s` and `t` of type `α`, if `t` is a subset of `s` and the relation `r` holds pairwise on the set `s`, then the relation `r` also holds pairwise on the set `t`. In other words, the pairwise property of a relation on a set is preserved under subset inclusion.
More concisely: If `r` is a relation on a type `α` such that `r` holds pairwise for all distinct elements of a set `s`, and `t` is a subset of `s`, then `r` holds pairwise for all distinct elements of `t`.
|
pairwise_disjoint_on
theorem pairwise_disjoint_on :
∀ {α : Type u_1} {ι : Type u_4} [inst : SemilatticeInf α] [inst_1 : OrderBot α] [inst_2 : LinearOrder ι]
(f : ι → α), Pairwise (Disjoint on f) ↔ ∀ ⦃m n : ι⦄, m < n → Disjoint (f m) (f n)
This theorem, `pairwise_disjoint_on`, states that for any types `α` and `ι` with the appropriate structures (`α` being a semilattice with a least element, and `ι` having a linear order), and for any function `f` from `ι` to `α`, the pairwise disjointness of the images under `f` is equivalent to stating that for any distinct `m` and `n` in `ι` with `m < n`, the images of `m` and `n` under `f` are disjoint. In other words, it provides a condition under which elements in the range of `f` are considered disjoint based on their originating indices in `ι`. Disjointness here means that any element `x` that is less than or equal to both `f(m)` and `f(n)` must be less than or equal to the bottom element of the semilattice.
More concisely: For a semilattice with least element α and linearly ordered type ι, a function f from ι to α has pairwise disjoint images if and only if for distinct m and n in ι with m < n, the images f(m) and f(n) are disjoint, meaning any x less than or equal to both is less than the least element of α.
|
Set.PairwiseDisjoint.elim_set
theorem Set.PairwiseDisjoint.elim_set :
∀ {α : Type u_1} {ι : Type u_4} {s : Set ι} {f : ι → Set α},
s.PairwiseDisjoint f → ∀ {i j : ι}, i ∈ s → j ∈ s → ∀ a ∈ f i, a ∈ f j → i = j
This theorem states that if a given set `s` of elements of type `ι` is pairwise disjoint under a function `f` from `ι` to sets of type `α`, then for any two elements `i` and `j` in `s` and any element `a` that belongs to both `f(i)` and `f(j)`, it must be the case that `i` equals `j`. In other words, no two distinct elements of the set `s` map under `f` to overlapping sets of type `α`.
More concisely: If `s` is a set of distinct elements from type `ι` with pairwise disjoint images under a function `f` from `ι` to sets of type `α`, then for any `i, j` in `s` and any `a` in `f(i) ∩ f(j)`, it follows that `i = j`.
|
Set.InjOn.pairwise_ne
theorem Set.InjOn.pairwise_ne :
∀ {α : Type u_1} {ι : Type u_4} {f : ι → α} {s : Set ι}, Set.InjOn f s → s.Pairwise fun x x_1 => f x ≠ f x_1 := by
sorry
This theorem, referred to as **Alias** of the forward direction of `Set.injOn_iff_pairwise_ne`, states that for any types `α` and `ι`, given a function `f` from `ι` to `α` and a set `s` of type `ι`, if the function `f` is injective on the set `s` (i.e., it doesn't map any two different elements of `s` to the same result), then the set `s` holds the property that for every pair of different elements `x` and `x_1` in `s`, the images of `x` and `x_1` under the function `f` are different. In other words, `f` preserves the distinctness of elements when applied to `s`. The theorem provides a condition under which we can guarantee that pairwise distinct elements in the set `s` will map to pairwise distinct results under the function `f`.
More concisely: If a function from a set to a type is injective on that set, then distinct elements in the set map to distinct images under the function.
|
Set.pairwiseDisjoint_fiber
theorem Set.pairwiseDisjoint_fiber :
∀ {α : Type u_1} {ι : Type u_4} (f : ι → α) (s : Set α), s.PairwiseDisjoint fun a => f ⁻¹' {a}
This theorem states that for any type `α`, any index type `ι`, any function `f` from `ι` to `α`, and any set `s` of type `α`, the set `s` is Pairwise Disjoint under the function that maps each element `a` of `α` to the preimage of `{a}` under `f`. In other words, for any two distinct elements of `s`, their preimages under `f` (i.e., the sets of elements that map to them) are disjoint.
More concisely: For any type `α`, index type `ι`, function `f` from `ι` to `α`, and set `s` of type `α`, if `a` and `b` are distinct elements of `s`, then the preimages `f⁁¹{a}` and `f⁁¹{b}` are disjoint subsets of `ι`.
|
Mathlib.Data.Set.Pairwise.Basic._auxLemma.16
theorem Mathlib.Data.Set.Pairwise.Basic._auxLemma.16 :
∀ {α : Type u} {s : Set α} {p : ↑s → Prop}, (∀ (x : ↑s), p x) = ∀ (x : α) (h : x ∈ s), p ⟨x, h⟩
This theorem states that for any type `α`, any set `s` of type `α`, and any property `p` that the elements of `s` might have, the statement that "for all elements `x` in `s`, `p` holds" is equivalent to the statement "for all elements `x` of type `α`, if `x` is in `s`, then `p` holds". The property `p` is here applied to `x` seen as an element of `s` (`{ val := x, property := h }`), where `h` is a proof that `x` is in `s`.
More concisely: For any type `α`, set `s` of `α`, and property `p`, the statements "for all `x` in `s`, `p(x)` holds" and "for all `x` of type `α`, if `x` is in `s` then `p(x)` holds" are logically equivalent.
|