The classical lower bound by the bounding number

Every family of fewer than boundingNumber permutations preserves a common conditionally convergent real series. Thus every rearranging family has size at least the bounding number. This statement does not presume that a rearranging family has already been constructed.

theorem NonMRR.extend_comp_perm (b : ℕ → ℝ) (l : ℕ → ℕ) (hl : Function.Injective l) (π : Equiv.Perm ℕ) : Function.extend l b 0 ∘ ⇑π = Function.extend (⇑(Equiv.symm π) ∘ l) b 0

Permuting a zero-padded series changes its placement to the inverse-permuted placement.

theorem NonMRR.not_isRearranging_of_cardinal_lt_boundingNumber (P : Set (Equiv.Perm ℕ)) (hP : Cardinal.mk ↑P < boundingNumber) : ¬IsRearranging P

A small family of permutations cannot rearrange every conditionally convergent real series.

theorem NonMRR.boundingNumber_le_cardinal_of_isRearranging {P : Set (Equiv.Perm ℕ)} (hP : IsRearranging P) : boundingNumber ≤ Cardinal.mk ↑P

Every rearranging family has cardinality at least the bounding number.

theorem NonMRR.aleph0_le_cardinal_of_isRearranging {P : Set (Equiv.Perm ℕ)} (hP : IsRearranging P) : Cardinal.aleph0 ≤ Cardinal.mk ↑P

In particular, every rearranging family is infinite.