English
Let B be a block with B nonempty. Then the product of the cardinality of B and the cardinality of its orbit under G equals the cardinality of X.
Русский
Пусть B — блок непуст, тогда произведение кардинальности B и кардинальности его орбиты равно кардинальности X.
LaTeX
$$Set.ncard B * Set.ncard (orbit G B) = Nat.card X$$
Lean4
/-- The cardinality of the ambient space is the product of the cardinality of a block
by the cardinality of the set of translates of that block -/
@[to_additive /-- The cardinality of the ambient space is the product of the cardinality of a block
by the cardinality of the set of translates of that block -/
]
theorem ncard_block_mul_ncard_orbit_eq (hB : IsBlock G B) (hB_ne : B.Nonempty) :
Set.ncard B * Set.ncard (orbit G B) = Nat.card X :=
by
obtain ⟨x, hx⟩ := hB_ne
rw [ncard_block_eq_relIndex hB hx, ← index_stabilizer, Subgroup.relIndex_mul_index (hB.stabilizer_le hx),
index_stabilizer_of_transitive]
