ciSup_pos

Mathlib.Order.ConditionallyCompleteLattice.Indexed

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

English

If p holds, the supremum over h ∈ p of f(h) equals f(h_p).

Русский

Если p истинно, то верхняя грань по p равна значению вWitness p.

LaTeX

$$ (hp : p) → iSup (fun h => f h) = f(hp)$$

Lean4

theorem ciSup_pos {p : Prop} {f : p → α} (hp : p) : ⨆ h : p, f h = f hp := by simp [hp]

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

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

Разделы

Аффилиация

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