English
For a multiset, the statement that card(s) equals 2 is equivalent to existence of two elements x,y with s = insert x (singleton y).
Русский
Для мультимножества утверждение, что размер равен 2, эквивалентно существованию двух элементов x,y с s = вставить x (одиночное y).
LaTeX
$$Eq s.card 2 ↔ ∃ x ∃ y, s = insert x (singleton y)$$
Lean4
/-- Characterisation of `2`-Freiman homs. -/
@[to_additive /-- Characterisation of `2`-Freiman isomorphisms. -/
]
theorem isMulFreimanIso_two :
IsMulFreimanIso 2 A B f ↔ BijOn f A B ∧ ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, ∀ d ∈ A, f a * f b = f c * f d ↔ a * b = c * d
where
mp hf := ⟨hf.bijOn, fun _ ha _ hb _ hc _ hd => hf.mul_eq_mul ha hb hc hd⟩
mpr hf := ⟨hf.1, by aesop (add simp card_eq_two)⟩
