English
For a fixed a, BlockMem G a forms a bounded order with a top element and a bottom element given by the universal block and the singleton block.
Русский
Для фиксированного a множество BlockMem(G,a) образует ограниченный по порядку набор: верхняя граница — универсальный блок, нижняя — блок-одиночка.
LaTeX
$$instance (a:X) : BoundedOrder (BlockMem G a) := ...$$
Lean4
/-- The type of blocks for a group action containing a given element is a bounded order. -/
@[to_additive /-- The type of blocks for an additive group action containing a given element is a
bounded order. -/
]
instance (a : X) : BoundedOrder (BlockMem G a)
where
top := ⟨Set.univ, Set.mem_univ a, .univ⟩
le_top := by
rintro ⟨B, ha, hB⟩
simp only [Subtype.mk_le_mk, le_eq_subset, subset_univ]
bot := ⟨{ a }, Set.mem_singleton a, IsBlock.singleton⟩
bot_le := by
rintro ⟨B, ha, hB⟩
simp only [Subtype.mk_le_mk, Set.le_eq_subset, Set.singleton_subset_iff]
exact ha
