English
Characterization of blocks in the atomised partition: t is a block iff nonempty and there exists Q ⊆ F such that t equals the set of i ∈ s that are synchronized with Q with respect to F.
Русский
Характеристика блоков атомизированного разбиения: t является блоком тогда и только тогда, когда он непуст и существует Q ⊆ F такое, что t совпадает с множеством i ∈ s, которые согласованы с Q по отношению F.
LaTeX
$$$ t \\in (atomise(s,F)).parts \\iff t.Nonempty \\land \\exists Q \\subseteq F, \\{i \\in s \\mid \\forall u \\in F, u \\in Q \\iff i \\in u\\} = t $$$
Lean4
theorem mem_atomise : t ∈ (atomise s F).parts ↔ t.Nonempty ∧ ∃ Q ⊆ F, {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u} = t := by
simp only [atomise, ofErase, bot_eq_empty, mem_erase, mem_image, nonempty_iff_ne_empty, mem_powerset]
