prod_mono_set'

Mathlib.Algebra.Order.BigOperators.Group.Finset

URI: https://scilib.ai/kg/mathlib#Finset.prod_mono_set'

← MathLib Explorer

English

The map s ↦ ∏_{x ∈ s} f(x) is monotone in s.

Русский

Отображение s ↦ ∏_{x ∈ s} f(x) монотонно по отношению к включению.

LaTeX

$$$\\text{Monotone}(s \\mapsto \\prod_{x \\in s} f(x))$$$

Lean4

@[to_additive sum_mono_set]
theorem prod_mono_set' (f : ι → M) : Monotone fun s ↦ ∏ x ∈ s, f x := fun _ _ hs ↦
  have := CanonicallyOrderedMul.toIsOrderedMonoid (α := M)
  prod_le_prod_of_subset' hs

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

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

Разделы

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

Аффилиация

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