not_mulDissociated — Mathlib

English

The negation of MulDissociated is characterized by the existence of two finite subsets with equal products (and not equal as sets).

Русский

Ложность MulDissociated характеризуется существованием двух конечных подмножеств с равными произведениями (и различными как множества).

LaTeX

$$$$ \neg \mathrm{MulDissociated}(s) \iff \exists t,u:\; t,u \subseteq s \land t \neq u \land \prod t = \prod u. $$$$

Lean4

@[to_additive (attr := simp)]
theorem not_mulDissociated :
    ¬MulDissociated s ↔ ∃ t : Finset α, ↑t ⊆ s ∧ ∃ u : Finset α, ↑u ⊆ s ∧ t ≠ u ∧ ∏ x ∈ t, x = ∏ x ∈ u, x := by
  simp [MulDissociated, InjOn]; aesop

Похожие утверждения