iInf_const_zero

Mathlib.Data.Nat.Lattice

URI: https://scilib.ai/kg/mathlib#Nat.iInf_const_zero

← MathLib Explorer

English

The infimum over a constant zero function equals zero: iInf_{ι} 0 = 0.

Русский

Нижняя грань константной функции 0 равна 0.

LaTeX

$$$iInf_{\iota} (0) = 0$$$

Lean4

/-- This combines `Nat.iInf_of_empty` with `ciInf_const`. -/
@[simp]
theorem iInf_const_zero {ι : Sort*} : ⨅ _ : ι, 0 = 0 :=
  (isEmpty_or_nonempty ι).elim (fun h ↦ by simp) fun h ↦ sInf_eq_zero.2 <| by simp

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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