English
Membership in the bound partition is equivalent to the existence of A with membership in Q.
Русский
Членство в связанном разбиении эквивалентно существованию A с членством в Q.
LaTeX
$$$b \in (P.bind Q).parts \iff \exists A, H_A, b \in (Q A H_A).parts$$$
Lean4
instance : Min (Finpartition a) :=
⟨fun P Q ↦
ofErase ((P.parts ×ˢ Q.parts).image fun bc ↦ bc.1 ⊓ bc.2)
(by
rw [supIndep_iff_disjoint_erase]
simp only [mem_image, and_imp, forall_exists_index, id, Prod.exists, mem_product, Finset.disjoint_sup_right,
mem_erase, Ne]
rintro _ x₁ y₁ hx₁ hy₁ rfl _ h x₂ y₂ hx₂ hy₂ rfl
rcases eq_or_ne x₁ x₂ with (rfl | xdiff)
· refine Disjoint.mono inf_le_right inf_le_right (Q.disjoint hy₁ hy₂ ?_)
intro t
simp [t] at h
exact Disjoint.mono inf_le_left inf_le_left (P.disjoint hx₁ hx₂ xdiff))
(by
rw [sup_image, id_comp, sup_product_left]
trans P.parts.sup id ⊓ Q.parts.sup id
· simp_rw [Finset.sup_inf_distrib_right, Finset.sup_inf_distrib_left]
rfl
· rw [P.sup_parts, Q.sup_parts, inf_idem])⟩
