mulSingle_mono — Mathlib

English

For a fixed index i, the map Pi.mulSingle i: f i → ∀ i, f i is monotone with respect to the product order.

Русский

Для фиксированного индекса i отображение Pi.mulSingle i: f i → ∀ i, f i монотонно по произведённому порядку.

LaTeX

$$$\mathrm{Monotone}(\mathrm{Pi.mulSingle}_i : f_i \to \forall i, f_i)$$$

Lean4

@[to_additive]
theorem mulSingle_mono : Monotone (Pi.mulSingle i : f i → ∀ i, f i) :=
  Function.update_mono

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