coe_iInf

Mathlib.Data.NNReal.Defs

URI: https://scilib.ai/kg/mathlib#NNReal.coe_iInf

← MathLib Explorer

English

The image of the infimum equals the infimum of the images.

Русский

Образ инфимума равен инфимуму образов.

LaTeX

$$$ (\\uparrow)(\\mathrm{iInf}\\ i \\mapsto s i) = \\mathrm{iInf}\\ i \\mapsto (\\uparrow)(s i). $$$

Lean4

@[norm_cast]
theorem coe_iInf {ι : Sort*} (s : ι → ℝ≥0) : (↑(⨅ i, s i) : ℝ) = ⨅ i, ↑(s i) := by
  rw [iInf, iInf, coe_sInf, ← Set.range_comp];
  rfl
    -- Short-circuit instance search

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

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

Разделы

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

Аффилиация

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