Theorems · Theorem · group theory

Monoid.CoprodI.lift_word_prod_nontrivial_of_not_empty

∀ {ι : Type u_1} {G : Type u_4} [inst : Group G] {H : ι → Type u_5} [inst_1 : (i : ι) → Group (H i)]
  (f : (i : ι) → H i →* G),
  (3 ≤ Cardinal.mk ι ∨ ∃ i, 3 ≤ Cardinal.mk (H i)) →
    ∀ {α : Type u_6} [inst_2 : MulAction G α] (X : ι → Set α),
      (∀ (i : ι), (X i).Nonempty) →
        Pairwise (Function.onFun Disjoint X) →
          (Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i) →
            ∀ [Nontrivial ι] {i j : ι} (w : Monoid.CoprodI.NeWord H i j), (Monoid.CoprodI.lift f) w.prod ≠ 1

Defined in

Mathlib.GroupTheory.CoprodI

Cited by

1 results in Mathlib

Foundations

Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupGroupMulActionNontrivial