Finset.AddETransform.card
theorem Finset.AddETransform.card :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : AddGroup α] (e : α) (x : Finset α × Finset α),
(Finset.addETransformLeft e x).1.card + (Finset.addETransformLeft e x).2.card +
((Finset.addETransformRight e x).1.card + (Finset.addETransformRight e x).2.card) =
x.1.card + x.2.card + (x.1.card + x.2.card)
This theorem states that for any type `α` with a decidable equality and an addition operation, and for any element `e` of type `α` and a pair of sets `x` of type α, the sum of the cardinalities of the sets resulting from an "e-transform" on `x` from the left and right (i.e., (s ∩ s +ᵥ e, t ∪ -e +ᵥ t) and (s ∪ s +ᵥ e, t ∩ -e +ᵥ t) respectively) is equal to twice the sum of the cardinalities of the original sets in `x`. In other words, performing an "e-transform" on the sets in `x` from both sides does not change the total cardinality.
More concisely: For any type `α` with decidable equality and addition operation, the cardinality sum of sets obtained by performing an "e-transform" on both sides remains unchanged, i.e., |(s ∩ s +ᵥ e) ∪ (s ∪ s +ᵥ e)| = 2|s| for any sets `s` in `α`.
|
Finset.MulETransform.card
theorem Finset.MulETransform.card :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Group α] (e : α) (x : Finset α × Finset α),
(Finset.mulETransformLeft e x).1.card + (Finset.mulETransformLeft e x).2.card +
((Finset.mulETransformRight e x).1.card + (Finset.mulETransformRight e x).2.card) =
x.1.card + x.2.card + (x.1.card + x.2.card)
This theorem states that for any type `α` that has a decidable equality and a group structure, and for any element `e` of this type and a pair of finite sets `x` of this type, the sum of the cardinalities of the two sets produced by the left and right e-transforms of `x` with respect to `e` is equal to twice the sum of the cardinalities of the sets in `x`. In other words, if `(s, t)` is the pair of sets in `x`, then the sum of the sizes of the sets `(s ∩ s • e, t ∪ e⁻¹ • t)` and `(s ∪ s • e, t ∩ e⁻¹ • t)` is equal to twice the sum of the sizes of `s` and `t`.
More concisely: For any decidably equal and group-structured type `α` and finite sets `s, t` of `α`, the cardinalities of the sets `s ∩ s • e` and `t ∪ e⁻¹ • t`, and `s ∪ s • e` and `t ∩ e⁻¹ • t`, respectively, sum up to twice the cardinalities of `s` and `t`.
|