Setoid.eq_of_mem_eqv_class
theorem Setoid.eq_of_mem_eqv_class :
∀ {α : Type u_1} {c : Set (Set α)},
(∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b) → ∀ {x : α} {b b' : Set α}, b ∈ c → x ∈ b → b' ∈ c → x ∈ b' → b = b'
This theorem states that for any type `α` and a set `c` containing subsets of `α`, given that each element `a` of `α` belongs to exactly one subset `b` that contains some element `x`, if an element `x` of `α` belongs to two different subsets `b` and `b'` that are both elements of `c`, then these two subsets must be equal. In other words, if we have a partition of a type into subsets, and an element is in two subsets of the partition, then these two subsets are the same. This theorem enforces the property of a partition where each element of the set being partitioned belongs to exactly one part of the partition.
More concisely: If `α` is a type, `c` is a set of subsets of `α`, and for all `a ∈ α`, there exists unique `b ∈ c` such that `a ∈ b`, then for all distinct `b, b' ∈ c` with `x ∈ b ∧ x ∈ b'`, we have `b = b'`.
|
Setoid.mem_classes
theorem Setoid.mem_classes : ∀ {α : Type u_1} (r : Setoid α) (y : α), {x | r.Rel x y} ∈ r.classes
This theorem states that, for any type `α`, any setoid `r` on `α`, and any element `y` of `α`, the set of all elements `x` in `α` that are related to `y` by the equivalence relation defined by `r` (`Setoid.Rel r x y`) is a member of the set of equivalence classes induced by `r` (`Setoid.classes r`). In other words, the set of all elements equivalent to a given element forms an equivalence class under the setoid.
More concisely: For any type `α`, setoid `r` on `α`, and `y` in `α`, `Setoid.Rel r x y` is a subset of `Setoid.classes r x`.
|
Setoid.classes_mkClasses
theorem Setoid.classes_mkClasses :
∀ {α : Type u_1} (c : Set (Set α)) (hc : Setoid.IsPartition c), (Setoid.mkClasses c ⋯).classes = c
This theorem states that, for any type 'α' and any set 'c' of sets of 'α' that forms a partition of 'α' (meaning that it divides 'α' into mutually exclusive, non-empty subsets), the equivalence classes generated by the equivalence relation defined by this partition are exactly equal to the original partitioning set 'c'. In other words, if we group elements of 'α' into equivalence classes based on the partition 'c', we end up with the same grouping as 'c'.
More concisely: For any type 'α' and partition 'c' of 'α', the equivalence classes of 'α' under the equivalence relation defined by 'c' are exactly the sets in 'c'.
|
IndexedPartition.index_some
theorem IndexedPartition.index_some :
∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) (i : ι), hs.index (hs.some i) = i := by
sorry
The theorem `IndexedPartition.index_some` states that for any types `ι` and `α`, and for any function `s` that maps from `ι` to a set of `α` such that `s` forms an indexed partition (as represented by `hs : IndexedPartition s`), if you pick some element from the `i`-th set in the partition (as represented by `hs.some i`), the index of that element in the partition (as represented by `hs.index (hs.some i)`) is indeed `i`. In other words, for each index `i`, the index of any element taken from the `i`-th subset in the partition is exactly `i`. This theorem is a fundamental property of indexed partitions.
More concisely: For any indexed partition `s` of type `ι → set α`, the element `hs.some i` in the `i`-th subset has index `i` within the partition (represented by `hs`).
|
Setoid.classes_eqv_classes
theorem Setoid.classes_eqv_classes : ∀ {α : Type u_1} {r : Setoid α} (a : α), ∃! b, b ∈ r.classes ∧ a ∈ b
This theorem states that, for any type `α` and any equivalence relation `r` on `α`, if you take an element `a` of type `α`, there exists precisely one set `b` such that `a` belongs to `b`. In other words, equivalence classes uniquely partition the type, meaning every element belongs to exactly one equivalence class.
More concisely: For any type `α` and equivalence relation `r` on `α`, the equivalence classes form a pairwise disjoint and exhaustive partition of `α`.
|
IndexedPartition.index_out'
theorem IndexedPartition.index_out' :
∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) (x : hs.Quotient),
hs.index (Quotient.out' x) = hs.index (hs.out x)
This theorem states that for any index type `ι`, any type `α`, any function `s` from `ι` to the set of `α`, and any `hs` that is an indexed partition of `s`, for any `x` in the quotient set associated with `hs`, the index of the output of the `Quotient.out'` function applied to `x` is equal to the index of the output of the `hs.out` function applied to `x`. In other words, these two methods of retrieving an element from a quotient set yield elements with the same index in the original partition.
More concisely: For any index type `ι`, function `s` from `ι` to a set, indexed partition `hs` of `s`, and quotient set element `x`, the indices of `s (hs.out x)` and `hs.out x` are equal.
|
IndexedPartition.proj_out
theorem IndexedPartition.proj_out :
∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) (x : hs.Quotient),
hs.proj (hs.out x) = x
The theorem `IndexedPartition.proj_out` states that for any types `ι` and `α`, and a function `s` from `ι` to a set of `α` such that `s` is an indexed partition, and for any quotient `x` of the indexed partition `hs`, the projection of the `out` function applied to `x` is equal to `x`. In simpler terms, this theorem asserts that the projection onto the quotient space recovers the original quotient element when applied to the representative of the equivalence class of the quotient.
More concisely: For any indexed partition `s` of type `ι → set α`, the projection `out` of a quotient `x` of `s` equals `x`.
|
Setoid.nonempty_of_mem_partition
theorem Setoid.nonempty_of_mem_partition :
∀ {α : Type u_1} {c : Set (Set α)}, Setoid.IsPartition c → ∀ {s : Set α}, s ∈ c → s.Nonempty
The theorem `Setoid.nonempty_of_mem_partition` states that for any type `α` and any collection `c` of sets of `α` that forms a partition of `α`, if a set `s` is a member of the partition `c`, then `s` is nonempty. In other words, in a valid partition of a type, there cannot be an empty set.
More concisely: For any type `α` and partition `c` of `α`, every set in `c` is nonempty.
|
IndexedPartition.mem_index
theorem IndexedPartition.mem_index :
∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (self : IndexedPartition s) (x : α), x ∈ s (self.index x) := by
sorry
This theorem, named "membership invariance for `index`," states that for every type `ι` and `α`, and every function `s` mapping `ι` to a set of `α`, given an `IndexedPartition` on `s` and a value `x` of type `α`, `x` is a member of the set `s` at the index given by the `index` function of the `IndexedPartition` applied to `x`. In other words, given any element `x` from the universe of `α`, it belongs to the set within the partition that the `index` function maps it to.
More concisely: For every function `s : ι → set α`, IndexedPartition `p : IndexedPartition ι (range s)`, and `x : α`, `x ∈ s (index p x)`.
|
IndexedPartition.mem_iff_index_eq
theorem IndexedPartition.mem_iff_index_eq :
∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) {x : α} {i : ι},
x ∈ s i ↔ hs.index x = i
The theorem `IndexedPartition.mem_iff_index_eq` states that for all types `ι` and `α`, for all function `s` mapping elements of `ι` to sets of `α` that forms an indexed partition `hs`, and for any element `x` of `α` and any index `i` of `ι`, `x` is an element of the set `s i` if and only if the index of `x` in the indexed partition `hs` is equal to `i`. In other words, given an indexed partition, an element belongs to a particular set within the partition exactly when its partition index matches the index of that set.
More concisely: For any indexed partition `hs` of type `ι → set α`, an element `x ∈ α` belongs to `s i` if and only if `i` is the index of `x` in the partition `hs`.
|
Setoid.exists_of_mem_partition
theorem Setoid.exists_of_mem_partition :
∀ {α : Type u_1} {c : Set (Set α)} (hc : Setoid.IsPartition c) {s : Set α},
s ∈ c → ∃ y, s = {x | (Setoid.mkClasses c ⋯).Rel x y}
This theorem states that for any set `α` and a partition `c` of `α`, if a set `s` is an element of the partition `c`, then there exists an element `y` in `α` such that `s` is the equivalence class of `y` under the equivalence relation defined by the partition `c`. In other words, every subset in a partition of a given set can be identified as the set of elements in the original set that are equivalent to some specific element under the equivalence relation corresponding to the partition.
More concisely: For any set `α` and partition `c`, if `s` is an element of `c`, then there exists an element `y` in `α` such that `s` is the equivalence class of `y` under relation `c`. (Or, every subset in a partition of a set can be identified as the equivalence class of some element in the original set.)
|
Setoid.eqv_class_mem
theorem Setoid.eqv_class_mem :
∀ {α : Type u_1} {c : Set (Set α)} (H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b) {y : α},
{x | (Setoid.mkClasses c H).Rel x y} ∈ c
This theorem states that for any type 'α' and any set 'c' of sets of 'α', if 'c' forms a partition of 'α' (i.e., every element 'a' of 'α' belongs to exactly one set 'b' in 'c' and 'b' is in 'c'), then for any element 'y' of 'α', the equivalence class of 'y' under the equivalence relation defined by 'c' is an element of 'c'. In other words, the equivalence classes generated by this partition also belong to the original partitioning set.
More concisely: For any partition 'c' of type 'α', the equivalence class of any 'y' in 'α' belongs to 'c'.
|
Setoid.eqv_classes_of_disjoint_union
theorem Setoid.eqv_classes_of_disjoint_union :
∀ {α : Type u_1} {c : Set (Set α)}, c.sUnion = Set.univ → c.PairwiseDisjoint id → ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
This theorem states that if we have a type `α` and a set `c` whose elements are sets of `α`, such that the union of all the sets in `c` is the universal set over `α` (i.e., `c` covers all of `α`), and every two different sets in `c` are disjoint (i.e., their intersection is empty), then `c` forms a partition of `α`. In other words, for any element `a` of `α`, there exists exactly one set `b` in `c` such that the element `a` belongs to the set `b`. This is a classical result in set theory. The concept of disjoint union is crucial here as it ensures that each element of `α` is placed in exactly one set in `c`, establishing the partition.
More concisely: If a family of pairwise disjoint sets covers the universal set, then it forms a partition.
|
IndexedPartition.some_mem
theorem IndexedPartition.some_mem :
∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (self : IndexedPartition s) (i : ι), self.some i ∈ s i
This theorem, named "membership invariance for `some`", states that for any types `ι` and `α`, and for a function `s` from `ι` to sets of `α`, if `self` is an indexed partition of `s` and `i` is an element of type `ι`, then the element produced by applying the `some` function to `i` (denoted as `self.some i`) is a member of the set `s i`. In simpler terms, this theorem guarantees that for each index in an indexed partition, the `some` function will always produce an element from the corresponding set in the partition.
More concisely: For any function `s : ι → sets α`, indexed partition `self : ∀ i : ι, s i → Prop`, and index `i : ι`, `some (self.val i) ∈ s i`.
|
IndexedPartition.eq_of_mem
theorem IndexedPartition.eq_of_mem :
∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α},
IndexedPartition s → ∀ {x : α} {i j : ι}, x ∈ s i → x ∈ s j → i = j
This theorem states that for any two indexes, denoted 'i' and 'j', from an indexed set 's' of type 'ι → Set α', if an element 'x' is a part of both 's i' and 's j' (i.e., 'x' is a member of the sets indexed by 'i' and 'j'), then 'i' must be equal to 'j'. Here, 'ι' is the type of the indexes, 'α' is the type of the elements in the sets, and 'IndexedPartition s' ensures that the sets are disjoint and their union covers the whole space. Thus, the theorem asserts that an element cannot be in two different sets of an indexed partition.
More concisely: For any indexed set 's' of type 'ι → Set α' with disjoint and exhaustive sets 's i' and 's j' of type 'Set α', if an element 'x' is a member of both 's i' and 's j', then 'i' = 'j'.
|
Setoid.empty_not_mem_classes
theorem Setoid.empty_not_mem_classes : ∀ {α : Type u_1} {r : Setoid α}, ∅ ∉ r.classes
This theorem states that the empty set is not an equivalence class. In other words, for any type `α` and any equivalence relation `r` on `α`, the set of equivalence classes of `r` does not contain the empty set. This means that there does not exist an element in `α` such that its equivalence class under `r` is empty.
More concisely: For any type `α` and equivalence relation `r` on `α`, the empty set is not an equivalence class under `r`.
|
Setoid.mkClasses_classes
theorem Setoid.mkClasses_classes : ∀ {α : Type u_1} (r : Setoid α), Setoid.mkClasses r.classes ⋯ = r
This theorem states that for any given equivalence relation `r` on a type `α`, if you construct a new equivalence relation using the set of equivalence classes for `r` as the partitions (via the function `Setoid.mkClasses`), the resulting equivalence relation is identical to the original equivalence relation `r`. In other words, forming equivalence classes and then using them to construct an equivalence relation does not change the equivalence relation.
More concisely: For any equivalence relation `r` on type `α`, the equivalence relation obtained by taking the set of equivalence classes as partitions using `Setoid.mkClasses` is equal to `r`.
|
Setoid.classes_inj
theorem Setoid.classes_inj : ∀ {α : Type u_1} {r₁ r₂ : Setoid α}, r₁ = r₂ ↔ r₁.classes = r₂.classes
This theorem states that two equivalence relations are equal if and only if their equivalence classes are the same. In other words, for any type `α` and any two equivalence relations `r₁` and `r₂` on `α`, `r₁` is equal to `r₂` precisely when the set of equivalence classes determined by `r₁` is the same as the set determined by `r₂`.
More concisely: Two equivalence relations on a type are equal if and only if their equivalence classes have the same elements.
|
IndexedPartition.some_index
theorem IndexedPartition.some_index :
∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) (x : α),
hs.setoid.Rel (hs.some (hs.index x)) x
The theorem `IndexedPartition.some_index` states that for any indexed partition `s` of a type `α` indexed by a type `ι`, and for any element `x` of type `α`, the equivalence relation induced by the indexed partition `s` relates the element `x` with the element obtained by applying the `some` operation (which selects some element from each subset of the partition) to the index of `x`. In other words, each element `x` of `α` is in the same partition subset as the one selected by the `some` operation on its index in the partition.
More concisely: For any indexed partition `s` of type `α` and element `x` of type `α`, `x` is in the same subset of `s` as the `some` element of the subset indexed by `x`.
|
Setoid.eq_of_mem_classes
theorem Setoid.eq_of_mem_classes :
∀ {α : Type u_1} {r : Setoid α} {x : α} {b : Set α},
b ∈ r.classes → x ∈ b → ∀ {b' : Set α}, b' ∈ r.classes → x ∈ b' → b = b'
This theorem states that for any given type `α` and an equivalence relation `r` on `α`, if an element `x` of `α` belongs to two equivalence classes `b` and `b'` under relation `r`, then the two equivalence classes `b` and `b'` must be the same. Essentially, this theorem is underlining the property of equivalence relations that each element belongs to exactly one equivalence class, hence if an element appears in two classes, those classes must be identical.
More concisely: For any equivalence relation `r` on type `α`, if `x` belongs to both equivalence classes `b` and `b'` under `r`, then `b = b'`.
|
Finpartition.isPartition_parts
theorem Finpartition.isPartition_parts : ∀ {α : Type u_1} (f : Finpartition Set.univ), Setoid.IsPartition ↑f.parts := by
sorry
This theorem states that for any given finite partition (`Finpartition`) of the universal set (`Set.univ`) over a certain type `α`, there correspondingly exists a setoid partition. Here, a setoid partition refers to a collection of sets that collectively cover the entire original set without any overlap, such that each element of the original set belongs to exactly one subset. Furthermore, this collection of sets does not contain the empty set.
More concisely: For any finite partition of a type `α`, there exists a corresponding setoid partition without the empty set.
|
Setoid.eq_eqv_class_of_mem
theorem Setoid.eq_eqv_class_of_mem :
∀ {α : Type u_1} {c : Set (Set α)} (H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b) {s : Set α} {y : α},
s ∈ c → y ∈ s → s = {x | (Setoid.mkClasses c H).Rel x y}
This theorem is about equivalence classes and partitioning of a set. It states that for a type `α` and a partition of `α` into a set `c` of subsets such that every element `a` of `α` belongs to exactly one subset `b` in `c`, if a subset `s` belongs to the partition `c` and an element `y` belongs to this subset `s`, then `s` is precisely the equivalence class of `y` under the equivalence relation defined by the partition `c`. In other words, `s` equals the set of all elements `x` that are related to `y` under the equivalence relation constructed from the partition.
More concisely: For any type `α` and partition `c` of `α` such that each element belongs to exactly one subset, every subset `s` in `c` equals the equivalence class of any element `y` in `s`, under the equivalence relation induced by `c`.
|
Setoid.eqv_classes_disjoint
theorem Setoid.eqv_classes_disjoint :
∀ {α : Type u_1} {c : Set (Set α)}, (∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b) → c.PairwiseDisjoint id
The theorem `Setoid.eqv_classes_disjoint` states that for any type `α` and a set `c` of sets of `α`, if every element `a` of `α` is in exactly one set `b` in `c` (i.e., `c` partitions `α`), then the sets in `c` are pairwise disjoint. In other words, no two different sets in `c` share a common element. This is a key property of any partition of a set.
More concisely: For any type `α` and set `c` of non-empty pairwise disjoint subsets of `α` that cover `α`, the subsets in `c` are equal to the equivalence classes of an equivalence relation on `α` where `a R b` if and only if `a` and `b` belong to the same set in `c`.
|
Setoid.eq_iff_classes_eq
theorem Setoid.eq_iff_classes_eq :
∀ {α : Type u_1} {r₁ r₂ : Setoid α}, r₁ = r₂ ↔ ∀ (x : α), {y | r₁.Rel x y} = {y | r₂.Rel x y}
The theorem states that in any given type `α`, two equivalence relations `r₁` and `r₂` are equal if and only if, for every element `x` of type `α`, the set of elements `y` that are related to `x` under `r₁` is the same as the set of elements `y` that are related to `x` under `r₂`. In other words, two equivalence relations are identical if they have identical equivalence classes for all elements of the type.
More concisely: Two equivalence relations on a type are equal if and only if they have the same equivalence classes for all elements of the type.
|
IndexedPartition.out_proj
theorem IndexedPartition.out_proj :
∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) (x : α),
hs.out (hs.proj x) = hs.some (hs.index x)
This theorem states that for any indexing type `ι`, type `α`, and a function `s` from `ι` to the set of `α` that forms an indexed partition `hs`, and any value `x` of type `α`, applying `out` function of `hs` to the projection of `x` under `hs` is the same as applying `some` function of `hs` to the index of `x` under `hs`. Essentially, it establishes a relationship between the `out`, `proj`, `some`, and `index` functions in an indexed partition.
More concisely: For any indexed partition `hs` of type `ι → set α`, and for all `x ∈ α`, `out (hs) (proj x hs) = some (hs) (index x hs)`.
|