iInf_neg

Mathlib.Order.CompleteLattice.Basic

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

English

If p is false, the infimum over h : p of f(h) is ⊤.

Русский

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

LaTeX

$$$$\neg p \rightarrow \bigwedge_{h : p} f(h) = \top.$$$$

Lean4

@[simp]
theorem iInf_neg {p : Prop} {f : p → α} (hp : ¬p) : ⨅ h : p, f h = ⊤ :=
  le_antisymm le_top <| le_iInf fun h => (hp h).elim

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

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

Разделы

Аффилиация

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