Theorems · Theorem · group theory

Set.powersetCard.isPretransitive_of_isMultiplyPretransitive

∀ (G : Type u_1) [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] {n : ℕ} [inst_2 : DecidableEq α],
  MulAction.IsMultiplyPretransitive G α n → MulAction.IsPretransitive G ↑(Set.powersetCard α n)

Defined in: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Cited by: 2 results in Mathlib
Foundations: Depth 88 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Group MulAction DecidableEq

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Finsetstatement · cited by 13,712
Set.Elemstatement · cited by 7,166
Groupstatement and proof · cited by 6,238
MulActionstatement and proof · cited by 1,294
Set.powersetCardstatement · cited by 100
MulAction.IsPretransitivestatement · cited by 94
MulAction.IsMultiplyPretransitivestatement and proof · cited by 33
MulAction.IsPretransitive.of_surjective_mapproof · cited by 7
Set.powersetCard.mulActionHom_of_embedding_surjectiveproof · cited by 1

Cited by2

Results whose statement or proof uses this declaration.

Set.powersetCard.isPretransitive_alternatingGroupproof · cited by 1
Set.powersetCard.isPretransitiveproof · cited by 1