English
If S and T are nonempty and S ×ˢ T ⊆ idRel, then there exists x with S = {x} and T = {x}.
Русский
Если S и T непустые и S ×ˢ T ⊆ idRel, то существует x такое, что S = {x} и T = {x}.
LaTeX
$$$S\\neq \\varnothing \\land T\\neq \\varnothing \\land S\\timesˢ T \\subseteq idRel \\Rightarrow \\exists x, S = \\{x\\} \\land T = \\{x\\}$$$
Lean4
theorem eq_singleton_prod_subset_idRel {X : Type*} {S T : Set X} (hS : S.Nonempty) (hT : T.Nonempty)
(h_diag : S ×ˢ T ⊆ idRel) : ∃ x, S = { x } ∧ T = { x } :=
by
obtain ⟨⟨x, hx⟩, ⟨y, hy⟩⟩ := eq_singleton_left_of_prod_subset_idRel hS hT h_diag,
eq_singleton_right_prod_subset_idRel hS hT h_diag
refine ⟨x, ⟨hx, ?_⟩⟩
rw [hy, Set.singleton_eq_singleton_iff]
exact
(Set.prod_subset_iff.mp h_diag x (by simp only [hx, Set.mem_singleton]) y
(by simp only [hy, Set.mem_singleton])).symm
