English
A pretransitive action on a nontrivial type is preprimitive iff the set of blocks containing a given element is a simple order (Additive variant).
Русский
Предпереводимое действие на ненулевом множестве: простейший порядок множества блоков вокруг элемента эквивалентен предпримитивности (аддитивная версия).
LaTeX
$$IsSimpleOrder (AddAction.BlockMem G a) ↔ AddAction.IsPreprimitive G X$$
Lean4
/-- A pretransitive action on a nontrivial type is preprimitive iff
the set of blocks containing a given element is a simple order -/
@[to_additive (attr := simp) /-- A pretransitive action on a nontrivial type is preprimitive iff
the set of blocks containing a given element is a simple order -/
]
theorem isSimpleOrder_blockMem_iff_isPreprimitive [IsPretransitive G X] [Nontrivial X] (a : X) :
IsSimpleOrder (BlockMem G a) ↔ IsPreprimitive G X :=
by
constructor
· intro h; let h_bot_or_top := h.eq_bot_or_eq_top
apply IsPreprimitive.of_isTrivialBlock_base a
intro B haB hB
rcases h_bot_or_top ⟨B, haB, hB⟩ with hB' | hB' <;> simp only [← Subtype.coe_inj] at hB'
· left; rw [hB']; exact Set.subsingleton_singleton
· right; rw [hB']; rfl
· intro hGX'; apply IsSimpleOrder.mk
rintro ⟨B, haB, hB⟩
simp only [← Subtype.coe_inj]
cases hGX'.isTrivialBlock_of_isBlock hB with
| inl h => simp [BlockMem.coe_bot, h.eq_singleton_of_mem haB]
| inr h => simp [BlockMem.coe_top, h]
