English
If a block B has too many translates relative to its orbit, then B is empty or a singleton.
Русский
Если блок B имеет слишком много переводов по отношению к орбите, то B пуст или состоит из одного элемента.
LaTeX
$$$\text{Finite}(X) \;\Rightarrow\; B \text{ subsingleton if } |X| < 2\cdot |\operatorname{orbit}(G,B)|$$$
Lean4
/-- If a block has too many translates, then it is a (sub)singleton -/
@[to_additive /-- If a block has too many translates, then it is a (sub)singleton -/
]
theorem subsingleton_of_card_lt [Finite X] (hB : IsBlock G B) (hB' : Nat.card X < 2 * Set.ncard (orbit G B)) :
B.Subsingleton :=
by
suffices Set.ncard B < 2 by
rw [Nat.lt_succ_iff, Set.ncard_le_one_iff_eq] at this
cases this with
| inl h => rw [h]; exact Set.subsingleton_empty
| inr h => obtain ⟨a, ha⟩ := h; rw [ha]; exact Set.subsingleton_singleton
cases Set.eq_empty_or_nonempty B with
| inl h => rw [h, Set.ncard_empty]; simp
| inr h =>
rw [← hB.ncard_block_mul_ncard_orbit_eq h, lt_iff_not_ge] at hB'
rw [← not_le]
exact fun hb ↦
hB'
(Nat.mul_le_mul_right _ hb)
/- The assumption `B.Finite` is necessary :
For G = ℤ acting on itself, a = 0 and B = ℕ, the translates `k • B` of the statement
are just `k + ℕ`, for `k ≤ 0`, and the corresponding intersection is `ℕ`, which is not a block.
(Remark by Thomas Browning) -/
