Translation-invariant subsets of a group

The regular translation action is transitive, so a subset invariant under every left translation is empty or universal. This is the final set-theoretic step in Gabriel's proof of Lemma 3.5.

theorem MagnitudeConjecture.CoveringAction.eq_empty_or_univ_of_add_left_invariant {A : Type u} [AddGroup A] (H : Set A) (hinv : ∀ (a b : A), b ∈ H ↔ a + b ∈ H) : H = ∅ ∨ H = Set.univ

A subset of an additive group which is invariant under every left translation is empty or the whole group.

theorem MagnitudeConjecture.CoveringAction.eq_empty_or_univ_of_mul_left_invariant {G : Type u} [Group G] (H : Set G) (hinv : ∀ (g h : G), h ∈ H ↔ g * h ∈ H) : H = ∅ ∨ H = Set.univ

Multiplicative form of translation transitivity.