English
The equality of product sets is characterized by either equality of factors or a joint emptiness pattern.
Русский
Равенство произведений множеств характеризуется либо равенством факторов, либо совместной пустотой.
LaTeX
$$$ s \times t = s_1 \times t_1 \iff (s = s_1 \land t = t_1) \lor ( (s = \emptyset \lor t = \emptyset) \land (s_1 = \emptyset \lor t_1 = \emptyset) ) $$$
Lean4
theorem prod_eq_prod_iff_of_nonempty (h : (s ×ˢ t).Nonempty) : s ×ˢ t = s₁ ×ˢ t₁ ↔ s = s₁ ∧ t = t₁ :=
by
constructor
· intro heq
have h₁ : (s₁ ×ˢ t₁ : Set _).Nonempty := by rwa [← heq]
rw [prod_nonempty_iff] at h h₁
rw [← fst_image_prod s h.2, ← fst_image_prod s₁ h₁.2, heq, eq_self_iff_true, true_and, ← snd_image_prod h.1 t, ←
snd_image_prod h₁.1 t₁, heq]
· grind
