Finpartition.ext
theorem Finpartition.ext :
∀ {α : Type u_1} {inst : Lattice α} {inst_1 : OrderBot α} {a : α} (x y : Finpartition a),
x.parts = y.parts → x = y
This theorem, `Finpartition.ext`, states that for any type `α` equipped with a lattice structure and a bottom element, and for any given element `a` of `α`, if we have two finite partitions `x` and `y` of `a`, then `x` is equal to `y` if and only if their parts are equal. In simpler terms, it asserts that two finite partitions of a given element are completely determined by their parts.
More concisely: For any lattice type `α` with bottom element, two finite partitions `x` and `y` of an element `a` are equal if and only if their parts are equal.
|
Finpartition.le
theorem Finpartition.le :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {a : α} (P : Finpartition a) {b : α},
b ∈ P.parts → b ≤ a
This theorem, named `Finpartition.le`, states that for any type `α` where `α` is equipped with a lattice structure and a minimal element (the bottom element), given any element `a` of type `α` and a finite partition `P` of `a`, if `b` is an element of the parts comprising the partition `P`, then `b` is less than or equal to `a`. In other words, every part of a finite partition is less than or equal to the whole.
More concisely: For any lattice `α` with a bottom element, and for any finite partition `P` of an element `a` in `α`, every part `b` of the partition satisfies `b ≤ a`.
|
Finpartition.ne_bot
theorem Finpartition.ne_bot :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {a : α} (P : Finpartition a) {b : α},
b ∈ P.parts → b ≠ ⊥
This theorem, `Finpartition.ne_bot`, states that for any type `α` that forms a lattice and has a least element (`⊥`), given a finite partition `P` of an element `a` of type `α`, any element `b` that is part of the partition `P` cannot be equal to the least element (`⊥`). In other words, no part of a finite partition of an element in a lattice is the bottom element of the lattice.
More concisely: For any lattice type `α` with a least element `⊥` and finite partition `P` of an element `a` in `α`, no part `b` of `P` equals `⊥`.
|
Finpartition.disjoint
theorem Finpartition.disjoint :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {a : α} (P : Finpartition a),
(↑P.parts).PairwiseDisjoint id
This theorem states that for any type `α` with a lattice structure and a least element, and given any `α`-element `a`, if `P` is a finite partition of `a` then the parts of `P` (obtained by coercing `P.parts` to a set) are pairwise disjoint under the identity function. In other words, for any distinct parts `p1` and `p2` of the partition `P`, their images under the identity function (which are just `p1` and `p2` themselves) are disjoint. This reflects the definition of a partition, where each part is disjoint from the others.
More concisely: Given a lattice `α` with a least element and a finite partition `P` of an `α`-element `a`, the parts of `P` are pairwise disjoint.
|
Finpartition.sum_card_parts
theorem Finpartition.sum_card_parts :
∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (P : Finpartition s),
(P.parts.sum fun i => i.card) = s.card
This theorem states that for any given type `α` with a decidable equality, and a finite set `s` of type `α`, if `P` is a partition of `s`, then the sum of the cardinalities (or sizes) of all the parts in `P` is equal to the size of `s`. In other words, if you break up a set into several non-overlapping parts, the total number of elements in all the parts combined is the same as the number of elements in the original set.
More concisely: For any finite type `α` with decidable equality, the sum of the sizes of the parts in any partition of a finite set `s` of type `α` equals the size of `s`.
|
Finpartition.not_bot_mem
theorem Finpartition.not_bot_mem :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {a : α} (self : Finpartition a), ⊥ ∉ self.parts := by
sorry
This theorem states that for any given finite partition (`Finpartition`) of an element `a` in a type `α`, where `α` is a lattice with a defined bottom element (`OrderBot α`), no element of the partition can be the bottom element. In other words, it's stating that the bottom element (`⊥`) cannot be a member (`∉`) of the parts (`self.parts`) of the partition.
More concisely: For any finite partition of a lattice with a bottom element, no part contains the bottom element.
|
Finpartition.supIndep
theorem Finpartition.supIndep :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {a : α} (self : Finpartition a), self.parts.SupIndep id
This theorem, `Finpartition.supIndep`, states that for any given type `α` in a lattice structure, which also has a bottom element (`OrderBot α`), and for any element `a` of type `α`, if `self` is a finite partition of `a` (`Finpartition a`), then the partition `self` is supremum-independent. In the context of this theorem, supremum-independence means that the supremum (or the least upper bound) of the partition does not depend on the order in which the elements are arranged.
More concisely: For any lattice type `α` with a bottom element and any finite partition `self` of an element `a` in `α`, the supremum of `self` is unique.
|