truncatedInf_of_notMem

Mathlib.Combinatorics.SetFamily.AhlswedeZhang

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

English

The truncatedInf of the empty set at any a is the bottom element ⊥.

Русский

УсечённыйInf пустого множества над любым a равен ⊥.

LaTeX

$$$\operatorname{truncatedInf} \emptyset \, a = \bot$$$

Lean4

theorem truncatedInf_of_notMem (h : a ∉ upperClosure s) : truncatedInf s a = ⊥ :=
  dif_neg h

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

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

Разделы

Аффилиация

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