mem_singleton — Mathlib

English

An element belongs to the singleton {y} iff it is equivalent to y.

Русский

Элемент принадлежит синглтонку {y} тогда и только тогда, когда он эквивалентен y.

LaTeX

$$$$ x \in \{ y \} \iff \operatorname{Equiv}(x,y) $$$$

Lean4

@[simp]
theorem mem_singleton {x y : PSet} : x ∈ ({ y } : PSet) ↔ Equiv x y :=
  mem_insert_iff.trans ⟨fun o => Or.rec id (fun n => absurd n (notMem_empty _)) o, Or.inl⟩

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