pair_eq_singleton_iff — Mathlib

English

Let x, y, z be sets. Then {x, y} = {z} if and only if x = z and y = z.

Русский

Пусть x, y, z — множества. Тогда {x, y} = {z} тогда и только тогда, когда x = z и y = z.

LaTeX

$$$ \{ x, y \} = \{ z \} \iff x = z \land y = z $$$

Lean4

@[simp]
theorem pair_eq_singleton_iff {x y z : ZFSet} : ({ x, y } : ZFSet) = { z } ↔ x = z ∧ y = z :=
  by
  refine ⟨fun h ↦ ?_, ?_⟩
  · rw [← mem_singleton, ← mem_singleton]
    simp [← h]
  · rintro ⟨rfl, rfl⟩
    exact pair_eq_singleton y

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