eq_singleton_right_prod_subset_idRel

English

If S and T are nonempty subsets of X and S ×ˢ T ⊆ idRel, then T is a singleton: ∃ x, T = {x}.

Русский

Если S и T непустые подмножества X и S ×ˢ T ⊆ idRel, то T — одиночное: ∃ x, T = {x}.

LaTeX

$$$S\\neq \\varnothing \\land T\\neq \\varnothing \\land S \\timesˢ T \\subseteq idRel \\Rightarrow \\exists x, T={x}$$$

Lean4

theorem eq_singleton_right_prod_subset_idRel {X : Type*} {S T : Set X} (hS : S.Nonempty) (hT : T.Nonempty)
    (h_diag : S ×ˢ T ⊆ idRel) : ∃ x, T = { x } :=
  by
  rw [Set.prod_subset_iff] at h_diag
  replace h_diag := fun x hx y hy => (h_diag y hy x hx).symm
  exact eq_singleton_left_of_prod_subset_idRel hT hS (prod_subset_iff.mpr h_diag)

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