truncatedSup_empty

Mathlib.Combinatorics.SetFamily.AhlswedeZhang

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

English

truncatedSup of the empty set at any a equals ⊤.

Русский

truncatedSup пустого множества в любой точке a равно ⊤.

LaTeX

$$truncatedSup(\\varnothing, a) = \\top$$

Lean4

@[simp]
theorem truncatedSup_empty (a : α) : truncatedSup ∅ a = ⊤ :=
  truncatedSup_of_notMem (by simp)

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

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

Разделы

Аффилиация

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