mem_pure_self

Mathlib.Data.Semiquot

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

English

The element obtained by get from q at p lies in q.

Русский

Элемент, полученный через get q p, принадлежит q.

LaTeX

$$$get\ q\ p \in q$$$

Lean4

theorem mem_pure_self (a : α) : a ∈ (pure a : Semiquot α) :=
  Set.mem_singleton a

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

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

Разделы

Аффилиация

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