iInf_pos

Mathlib.Order.CompleteLattice.Basic

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

English

Let p be a proposition and f : p → α. If hp is a proof of p, then the infimum over h : p of f(h) equals f(hp).

Русский

Пусть p — proposition и f : p → α. Если есть доказательство hp, то ⨅_{h : p} f(h) = f(hp).

LaTeX

$$$$\bigwedge_{h : p} f(h) = f(h_p),$$$$

Lean4

@[simp]
theorem iInf_pos {p : Prop} {f : p → α} (hp : p) : ⨅ h : p, f h = f hp :=
  le_antisymm (iInf_le _ _) (le_iInf fun _ => le_rfl)

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

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

Разделы

Аффилиация

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