exists_eq_singleton_of_prod_subset_id

English

If s,t ⊆ α are nonempty and s × t ⊆ id, then there exists x with s = {x} and t = {x}.

Русский

Если s и t непустые подмножества α и s × t ⊆ id, то существует x такое, что s = {x} и t = {x}.

LaTeX

$$s.Nonempty \rightarrow t.Nonempty \rightarrow s \times t \subseteq \mathrm{SetRel.id} \Rightarrow \exists x, s = {x} \land t = {x}$$

Lean4

theorem exists_eq_singleton_of_prod_subset_id {s t : Set α} (hs : s.Nonempty) (ht : t.Nonempty)
    (hst : s ×ˢ t ⊆ SetRel.id) : ∃ x, s = { x } ∧ t = { x } :=
  by
  obtain ⟨a, ha⟩ := hs
  obtain ⟨b, hb⟩ := ht
  simp only [Set.prod_subset_iff, mem_id] at hst
  obtain rfl := hst _ ha _ hb
  simp only [Set.eq_singleton_iff_unique_mem, and_assoc]
  exact ⟨a, ha, (hst · · _ hb), hb, (hst _ ha · · |>.symm)⟩

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