eq_singleton_left_of_prod_subset_idRel

English

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

Русский

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

LaTeX

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

Lean4

theorem eq_singleton_left_of_prod_subset_idRel {X : Type*} {S T : Set X} (hS : S.Nonempty) (hT : T.Nonempty)
    (h_diag : S ×ˢ T ⊆ idRel) : ∃ x, S = { x } :=
  by
  rcases hS, hT with ⟨⟨s, hs⟩, ⟨t, ht⟩⟩
  refine ⟨s, eq_singleton_iff_nonempty_unique_mem.mpr ⟨⟨s, hs⟩, fun x hx ↦ ?_⟩⟩
  rw [prod_subset_iff] at h_diag
  replace hs := h_diag s hs t ht
  replace hx := h_diag x hx t ht
  simp only [idRel, mem_setOf_eq] at hx hs
  rwa [← hs] at hx

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