supIndep_empty

Mathlib.Order.SupIndep

URI: https://scilib.ai/kg/mathlib#Finset.supIndep_empty

English

The empty finite set is trivially sup-independent for any f.

Русский

Пустое множество индексов является тривиально SupIndep.

LaTeX

$$$\\bigl( { } : Finset \\; ι \\bigr).SupIndep f$$$

Lean4

@[simp]
theorem supIndep_empty (f : ι → α) : (∅ : Finset ι).SupIndep f := fun _ _ a ha => (notMem_empty a ha).elim

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

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

Разделы

Аффилиация

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