mulDissociated_iff_sum_eq_subsingleton

English

In a commutative group α, a set s is MulDissociated iff for every a ∈ α, the collection {t ⊆ s | ∑ x∈t x = a} is subsingleton.

Русский

В коммутативной группе α множество s является MulDissociated тогда и только тогда, когда для каждого a ∈ α множество {t ⊆ s | ∑ x∈t x = a} является пододиночным.

LaTeX

$$$$ \operatorname{MulDissociated}(s) \iff \forall a, \{t : \mathrm{Finset}\;\alpha \mid t \subseteq s \land \sum_{x\in t} x = a\}.\mathrm{Subsingleton}. $$$$

Lean4

@[to_additive]
theorem mulDissociated_iff_sum_eq_subsingleton :
    MulDissociated s ↔ ∀ a, {t : Finset α | ↑t ⊆ s ∧ ∏ x ∈ t, x = a}.Subsingleton :=
  ⟨fun hs _ _t ht _u hu ↦ hs ht.1 hu.1 <| ht.2.trans hu.2.symm, fun hs _t ht _u hu htu ↦ hs _ ⟨ht, htu⟩ ⟨hu, rfl⟩⟩

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