truncatedSup_of_notMem

Mathlib.Combinatorics.SetFamily.AhlswedeZhang

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

English

If a ∉ lowerClosure(s), then truncatedSup s a = ⊤.

Русский

Если a не принадлежит lowerClosure(s), то truncatedSup s a = ⊤.

LaTeX

$$a \\notin lowerClosure(s) \\Rightarrow truncatedSup(s,a) = \\top$$

Lean4

theorem truncatedSup_of_notMem (h : a ∉ lowerClosure s) : truncatedSup s a = ⊤ :=
  dif_neg h

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

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

Разделы

Аффилиация

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