sized_empty

Mathlib.Data.Finset.Slice

URI: https://scilib.ai/kg/mathlib#Set.sized_empty

English

The empty set is Sized r for any r.

Русский

Пустое множество является Sized r для любого r.

LaTeX

$$$$ (\emptyset : Set (Finset α)).Sized r $$$$

Lean4

@[simp]
theorem sized_empty : (∅ : Set (Finset α)).Sized r := by simp [Sized]

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

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

Разделы

Аффилиация

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