toFinset_some

Mathlib.Data.Finset.PImage

URI: https://scilib.ai/kg/mathlib#Part.toFinset_some

English

The toFinset of some a is the singleton {a}.

Русский

ToFinset (некоторое a) равно одиночному множеству {a}.

LaTeX

$$$(\text{some } a).toFinset = \{ a \}$.$$

Lean4

@[simp]
theorem toFinset_some {a : α} [Decidable (some a).Dom] : (some a).toFinset = { a } := by simp [toFinset]

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

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

Разделы

Аффилиация

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