prod_mono — Mathlib

English

If f1 ≤ f2 and g1 ≤ g2 are monotone maps, then f1.prod g1 ≤ f2.prod g2.

Русский

Если f1 ≤ f2 и g1 ≤ g2 — монотонные отображения, то f1.prod g1 ≤ f2.prod g2.

LaTeX

$$$ f_1 \le f_2 \Rightarrow g_1 \le g_2 \Rightarrow f_1.\mathrm{prod}\, g_1 \le f_2.\mathrm{prod}\, g_2. $$$

Lean4

@[mono]
theorem prod_mono {f₁ f₂ : α →o β} (hf : f₁ ≤ f₂) {g₁ g₂ : α →o γ} (hg : g₁ ≤ g₂) : f₁.prod g₁ ≤ f₂.prod g₂ := fun _ =>
  Prod.le_def.2 ⟨hf _, hg _⟩

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