mem_pure'

Mathlib.Data.Semiquot

URI: https://scilib.ai/kg/mathlib#Semiquot.mem_pure'

English

For all a,b, a lies in the singleton generated by b if and only if a = b.

Русский

Для всех a,b: a принадлежит чистому b тогда и только тогда, когда a = b.

LaTeX

$$$a \in \{b\} \iff a = b$$$

Lean4

@[simp]
theorem mem_pure' {a b : α} : a ∈ Semiquot.pure b ↔ a = b :=
  Set.mem_singleton_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru