Theorems · Theorem · group theory

Equiv.Perm.disjoint_support_closure_of_disjoint_support

∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Fintype α] {S T : Set (Equiv.Perm α)},
  (∀ a ∈ S, ∀ b ∈ T, Disjoint a.support b.support) →
    ∀ a ∈ Subgroup.closure S, ∀ b ∈ Subgroup.closure T, Disjoint a.support b.support

Defined in

Mathlib.GroupTheory.Perm.Finite

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEqFintype