coe_iInf

Mathlib.Order.Sublocale

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

English

The underlying value of iInf f equals iInf of the underlying values: (iInf f).val = iInf (f i).val.

Русский

Значение iInf f равно инфимуму значений f i: (iInf f).val = ⨅ i, (f i).val.

LaTeX

$$$(\operatorname{iInf} i, f(i)).\text{val} = \operatorname{iInf}_i (f(i)).\text{val}$$$

Lean4

@[simp, norm_cast]
theorem coe_iInf (f : ι → S) : (⨅ i, f i).val = ⨅ i, (f i).val := by simp [iInf, ← range_comp, Function.comp_def]

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

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

Разделы

Аффилиация

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