English
Given a setoid s on α and a finite subset x ⊆ α, the finpartition of x is obtained by grouping elements of x into blocks that are the equivalence classes of s restricted to x.
Русский
При заданном отношении эквивалентности s на α и конечном подмножестве x, разбиение x образуется группировкой элементов x в классы эквивалентности относительного s на x.
LaTeX
$$$\\text{ofSetSetoid}(s, x)$ is the finpartition of x with parts $x\\_image(a \\mapsto \\{b\\in x\\mid s\\,r\\,a\\,b\\})$.$$
Lean4
/-- A setoid over a finite type induces a finpartition of the type's elements,
where the parts are the setoid's equivalence classes. -/
@[simps -isSimp]
def ofSetSetoid (s : Setoid α) (x : Finset α) [DecidableRel s.r] : Finpartition x
where
parts := x.image fun a ↦ {b ∈ x | s.r a b}
supIndep :=
by
suffices ∀ (a b c d : α), s a d → s b d → (s a c ↔ s b c)
by
simp only [supIndep_iff_pairwiseDisjoint, Set.PairwiseDisjoint, Set.Pairwise, coe_image, Set.mem_image, mem_coe,
ne_eq, onFun, id_eq, disjoint_iff_ne, forall_mem_not_eq, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
mem_filter, not_and, filter_inj', not_forall, @not_imp_comm (_ ↔ _), Decidable.not_not]
intro _ _ _ _ _ _ _ _ ha _ hb
exact ⟨(s.trans' hb <| s.trans' (s.symm' ha) ·), (s.trans' ha <| s.trans' (s.symm' hb) ·)⟩
simp +contextual [← Quotient.eq]
sup_parts := by
ext a
simp_rw [sup_image, id_comp, mem_sup, mem_filter]
refine ⟨(·.choose_spec.2.1), fun _ ↦ by use a⟩
bot_notMem := by
suffices ∀ x₁ ∈ x, ∃ x₂ ∈ x, s x₁ x₂ by simpa [filter_eq_empty_iff]
intro x _
use x
