pi_mono

Mathlib.Order.Filter.Pi

URI: https://scilib.ai/kg/mathlib#Filter.pi_mono

English

If for all i, f1(i) ≤ f2(i), then the indexed product satisfies pi f1 ≤ pi f2.

Русский

Если для каждого i выполнено f1(i) ≤ f2(i), то произведение по индексу удовлетворяет pi f1 ≤ pi f2.

LaTeX

$$(\forall i, f1 i ≤ f2 i) \Rightarrow (\pi f1) ≤ (\pi f2).$$

Lean4

@[mono]
theorem pi_mono (h : ∀ i, f₁ i ≤ f₂ i) : pi f₁ ≤ pi f₂ :=
  iInf_mono fun i => comap_mono <| h i

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

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

Разделы

Аффилиация

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