mem_pure

Mathlib.Data.Semiquot

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

English

For all a,b, a ∈ pure b in Semiquot α iff a = b.

Русский

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

LaTeX

$$$ a \\in \\text{pure}(b) \\iff a = b $$$

Lean4

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

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

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

Разделы

Аффилиация

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