English
Definition ofSetoid: a finpartition of the universal finite set induced by a setoid on α.
Русский
Определение ofSetoid: конечное разбиение универсума на основе множества эквивалентности на α.
LaTeX
$$$\\text{ofSetoid}(s) \\;:\\; Finpartition(\\text{univ})$$$
Lean4
/-- Cuts `s` along the finsets in `F`: Two elements of `s` will be in the same part if they are
in the same finsets of `F`. -/
def atomise (s : Finset α) (F : Finset (Finset α)) : Finpartition s :=
ofErase (F.powerset.image fun Q ↦ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t})
(Set.PairwiseDisjoint.supIndep fun x hx y hy h ↦
disjoint_left.mpr fun z hz1 hz2 ↦
h (by
rw [mem_coe, mem_image] at hx hy
obtain ⟨Q, hQ, rfl⟩ := hx
obtain ⟨R, hR, rfl⟩ := hy
suffices h' : Q = R by
subst h'
exact of_eq_true (eq_self ({i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}))
rw [id, mem_filter] at hz1 hz2
rw [mem_powerset] at hQ hR
ext i
refine ⟨fun hi ↦ ?_, fun hi ↦ ?_⟩
· rwa [hz2.2 _ (hQ hi), ← hz1.2 _ (hQ hi)]
· rwa [hz1.2 _ (hR hi), ← hz2.2 _ (hR hi)]))
(by
refine (Finset.sup_le fun t ht ↦ ?_).antisymm fun a ha ↦ ?_
· rw [mem_image] at ht
obtain ⟨A, _, rfl⟩ := ht
exact s.filter_subset _
· rw [mem_sup]
refine
⟨{i ∈ s | ∀ t ∈ F, t ∈ {u ∈ F | a ∈ u} ↔ i ∈ t}, mem_image_of_mem _ (mem_powerset.2 <| filter_subset _ _),
mem_filter.2 ⟨ha, fun t ht ↦ ?_⟩⟩
rw [mem_filter]
exact and_iff_right ht)
