sup'_div₀

Mathlib.Algebra.Order.GroupWithZero.Finset

URI: https://scilib.ai/kg/mathlib#Finset.sup'_div₀

← MathLib Explorer

English

For a > 0, dividing the supremum by a equals the supremum of the quotients: sup' f / a = sup' (f i / a).

Русский

При a > 0 имеем: sup' f / a = sup' (f i / a).

LaTeX

$$$\sup'_{i\in s} f(i) / a = \sup'_{i\in s} (f(i)/a).$$$

Lean4

theorem sup'_div₀ [MulPosReflectLT G₀] (ha : 0 < a) (f : ι → G₀) (s : Finset ι) (hs) :
    s.sup' hs f / a = s.sup' hs fun i ↦ f i / a :=
  map_finset_sup' (OrderIso.divRight₀ _ ha) hs f

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

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

Разделы

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

Аффилиация

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