ciInf_pos

Mathlib.Order.ConditionallyCompleteLattice.Indexed

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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