English
There is a partial order on partitions given by refinement, turning the set of partitions into a poset.
Русский
Существует частичное упорядочение разбиений по refining, образующее частичный порядок.
LaTeX
$$$\\text{PartialOrder}((\\text{Subtype} \\; \\text{IsPartition}))$ with le defined by refinement$$
Lean4
/-- Defining a partial order on partitions as the partial order on their induced
equivalence relations. -/
instance partialOrder : PartialOrder (Subtype (@IsPartition α))
where
le := (· ≤ ·)
lt x y := x ≤ y ∧ ¬y ≤ x
le_refl _ := @le_refl (Setoid α) _ _
le_trans _ _ _ := @le_trans (Setoid α) _ _ _ _
lt_iff_le_not_ge _ _ := Iff.rfl
le_antisymm x y hx
hy := by
let h := @le_antisymm (Setoid α) _ _ _ hx hy
rw [Subtype.ext_iff, ← classes_mkClasses x.1 x.2, ← classes_mkClasses y.1 y.2, h]
