mem_singleton

Mathlib.Data.Finmap

URI: https://scilib.ai/kg/mathlib#Finmap.mem_singleton

English

An element x belongs to the singleton Finmap exactly when x equals the key of that singleton.

Русский

Элемент x принадлежит singleton тогда и только тогда, когда x равно ключу одиночного элемента.

LaTeX

$$$$ x \in singleton y b \iff x = y $$$$

Lean4

@[simp]
theorem mem_singleton (x y : α) (b : β y) : x ∈ singleton y b ↔ x = y := by simp [singleton, mem_def]

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

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

Разделы

Аффилиация

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