prod_le_prod — Mathlib

English

Let f,g: ι → Cardinal with f(i) ≤ g(i) for all i. Then ∏_{i∈ι} f(i) ≤ ∏_{i∈ι} g(i).

Русский

Пусть f,g: ι → кардинальные числа так, что f(i) ≤ g(i) для всех i. Тогда ∏_{i∈ι} f(i) ≤ ∏_{i∈ι} g(i).

LaTeX

$$$\forall \iota\,(f,g: \iota \to \mathrm{Cardinal}),\ (\forall i:\iota,\ f(i) \le g(i))\;\Rightarrow\; \prod_{i:\iota} f(i) \le \prod_{i:\iota} g(i)$$$

Lean4

theorem prod_le_prod {ι} (f g : ι → Cardinal) (H : ∀ i, f i ≤ g i) : prod f ≤ prod g :=
  ⟨Embedding.piCongrRight fun i => Classical.choice <| by have := H i; rwa [← mk_out (f i), ← mk_out (g i)] at this⟩

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