English
A block system is a partition of X into blocks stable under the G-action: it is a set of blocks ℬ such that every B ∈ ℬ is a block and ℬ partitions X.
Русский
Система блоков — это разбиение X на блоки, согласованное с действием G: множество ℬ блоков таково, что каждый блок принадлежит ℬ и ℬ образует разбиение X.
LaTeX
$$$\\text{IsBlockSystem } G\\; \\mathcal{B} := (Setoid.IsPartition\\mathcal{B}) \\wedge (\\forall\\; B\\in\\mathcal{B}, IsBlock\\ G\\ B)$$$
Lean4
/-- For `SMul G X`, a block system of `X` is a partition of `X` into blocks
for the action of `G` -/
@[to_additive /-- For `VAdd G X`, a block system of `X` is a partition of `X` into blocks
for the additive action of `G` -/
]
def IsBlockSystem (ℬ : Set (Set X)) :=
Setoid.IsPartition ℬ ∧ ∀ ⦃B⦄, B ∈ ℬ → IsBlock G B
