toFinset_none

Mathlib.Data.Finset.PImage

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

English

The toFinset of the empty Part is the empty Finset.

Русский

Peрeделение toFinset пустого элемента равно пустому Finset.

LaTeX

$$$\text{none.toFinset} = \emptyset$.$$

Lean4

@[simp]
theorem toFinset_none [Decidable (none : Part α).Dom] : none.toFinset = (∅ : Finset α) := by simp [toFinset]

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

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

Разделы

Аффилиация

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