English
For a finite x and s a Setoid on α, the membership of b in the a-th part of the induced partition is equivalent to a ∈ x, b ∈ x and a is related to b by s.
Русский
Для множества x и отношения эквивалентности s на α, членство b в блоке a-ой части разбиения эквивалентно a ∈ x, b ∈ x и a ~ b.
LaTeX
$$$ b \\in (ofSetSetoid(s, x)).part(a) \\iff a\\in x \\wedge b\\in x \\wedge s(a,b) $$
Lean4
theorem mem_part_ofSetSetoid_iff_rel {s : Setoid α} (x : Finset α) [DecidableRel s.r] {b : α} :
b ∈ (ofSetSetoid s x).part a ↔ a ∈ x ∧ b ∈ x ∧ s a b :=
by
suffices (∃ a₁ ∈ x, (b ∈ x ∧ s a₁ b) ∧ a ∈ x ∧ s a₁ a) ↔ a ∈ x ∧ b ∈ x ∧ s a b by
simpa [mem_part_iff_exists, ofSetSetoid_parts]
exact
⟨fun ⟨c, _, ⟨hb, hcb⟩, ⟨ha, hca⟩⟩ ↦ ⟨ha, hb, s.trans' (s.symm' hca) hcb⟩, fun h ↦
⟨a, ⟨h.1, ⟨⟨h.2.1, h.2.2⟩, ⟨h.1, s.refl _⟩⟩⟩⟩⟩
