iSup_neg

Mathlib.Order.CompleteLattice.Basic

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

English

If p is false, the supremum over h : p of f(h) is ⊥.

Русский

Если p ложно, то ⨆_{h : p} f(h) = ⊥.

LaTeX

$$$$\neg p \rightarrow \bigvee_{h : p} f(h) = \bot.$$$$

Lean4

@[simp]
theorem iSup_neg {p : Prop} {f : p → α} (hp : ¬p) : ⨆ h : p, f h = ⊥ :=
  le_antisymm (iSup_le fun h => (hp h).elim) bot_le

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

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

Разделы

Аффилиация

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