English
There is an equivalence between the existence of a pair a0,b0 with UniqueMul A B a0 b0 and the existence of a g with a unique ab in A×ˢB such that ab.1*ab.2 = g.
Русский
Существование пары a0,b0 с UniqueMul эквивалентно существованию g с уникальным ab в A×ˢB и ab.1*ab.2 = g.
LaTeX
$$$(\\exists a_0,b_0\\in G, a_0\\in A \\land b_0\\in B \\land UniqueMul A B a_0 b_0) \\iff \\exists g:\\,G,\\exists!\\; ab,\\; ab\\in A×ˢB \\land ab.1*ab.2=g$$$
Lean4
@[to_additive]
theorem exists_iff_exists_existsUnique :
(∃ a0 b0 : G, a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0) ↔ ∃ g : G, ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = g :=
⟨fun ⟨_, _, hA, hB, h⟩ ↦ ⟨_, (iff_existsUnique hA hB).mp h⟩, fun ⟨g, h⟩ ↦
by
have h' := h
rcases h' with ⟨⟨a, b⟩, ⟨hab, rfl, -⟩, -⟩
obtain ⟨ha, hb⟩ := Finset.mem_product.mp hab
exact ⟨a, b, ha, hb, (iff_existsUnique ha hb).mpr h⟩⟩
