ciSup_neg

Mathlib.Order.ConditionallyCompleteLattice.Indexed

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

← MathLib Explorer

English

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

Русский

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

LaTeX

$$¬p → iSup (fun h => f h) = sSup (∅ : Set α)$$

Lean4

theorem ciSup_neg {p : Prop} {f : p → α} (hp : ¬p) : ⨆ (h : p), f h = sSup (∅ : Set α) :=
  by
  rw [iSup]
  congr
  rwa [range_eq_empty_iff, isEmpty_Prop]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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