iInf_const

Mathlib.Order.CompleteLattice.Basic

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

English

If ι is nonempty, the infimum of a constant a over ι equals a: ⨅ i, a = a.

Русский

Если ι непусто, то ⨅ i a = a.

LaTeX

$$$\\\\iInf i\, a = a$$$

Lean4

theorem iInf_const [Nonempty ι] : ⨅ _ : ι, a = a :=
  @iSup_const αᵒᵈ _ _ a _

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

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

Разделы

Аффилиация

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