English
The negation of MulDissociated is equivalent to the existence of disjoint finite subsets t and u ⊆ s with t ≠ u and equal products, i.e., ∏ t = ∏ u.
Русский
Отрицание MulDissociated эквивалентно существованию непересекающихся конечных подмножеств t, u ⊆ s с t ≠ u и равными произведениями, т.е. ∏ t = ∏ u.
LaTeX
$$$$ \neg \mathrm{MulDissociated}(s) \iff \exists t,u:\; t,u \subseteq s \land \mathrm{Disjoint}(t,u) \land t \neq u \land \prod t = \prod u. $$$$
Lean4
@[to_additive]
theorem not_mulDissociated_iff_exists_disjoint :
¬MulDissociated s ↔ ∃ t u : Finset α, ↑t ⊆ s ∧ ↑u ⊆ s ∧ Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a := by
classical
refine not_mulDissociated.trans ⟨?_, fun ⟨t, u, ht, hu, _, htune, htusum⟩ ↦ ⟨t, ht, u, hu, htune, htusum⟩⟩
rintro ⟨t, ht, u, hu, htu, h⟩
refine
⟨t \ u, u \ t, ?_, ?_, disjoint_sdiff_sdiff, sdiff_ne_sdiff_iff.2 htu,
Finset.prod_sdiff_eq_prod_sdiff_iff.2 h⟩ <;>
push_cast <;>
exact diff_subset.trans ‹_›
