coe_iInf

Mathlib.Data.ENat.Lattice

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

English

Assume ι is nonempty. Then ↑(⨅ i, f i) = ⨅ i, (f i : ℕ∞).

Русский

Пусть ι ненулевой; тогда приводимый к ENat нижний предел: ↑(⨅ i, f i) = ⨅ i, (f i : ℕ∞).

LaTeX

$$$\uparrow(\inf_i f(i)) = \inf_i (f(i) : \mathbb{N}_\infty)$$$

Lean4

@[norm_cast]
theorem coe_iInf [Nonempty ι] : ↑(⨅ i, f i) = ⨅ i, (f i : ℕ∞) :=
  WithTop.coe_iInf (OrderBot.bddBelow _)

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

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

Разделы

Аффилиация

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