ciInf_neg

Mathlib.Order.ConditionallyCompleteLattice.Indexed

URI: https://scilib.ai/kg/mathlib#ciInf_neg

English

If not p, the infimum over h ∈ p of f(h) equals the infimum of the empty set.

Русский

Если не p, то нижняя грань по p равна нижней грани пустого множества.

LaTeX

$$¬p → iInf (fun h => f h) = sInf (∅ : Set α)$$

Lean4

theorem ciInf_neg {p : Prop} {f : p → α} (hp : ¬p) : ⨅ (h : p), f h = sInf (∅ : Set α) :=
  ciSup_neg (α := αᵒᵈ) hp

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

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

Разделы

Аффилиация

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