Theorems · Theorem · group theory

SubMulAction.IsPretransitive.isPretransitive_ofFixingSubgroup_inter

∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s : Set α},
  MulAction.IsPretransitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s) →
    ∀ {g : M},
      s ∪ g • s ≠ ⊤ →
        MulAction.IsPretransitive ↥(fixingSubgroup M (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup M (s ∩ g • s))

A pretransitivity criterion.

Defined in

Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Cited by

2 results in Mathlib

Foundations

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

Assumes

GroupMulAction