prod_le_prod — Mathlib

English

Under NeBot assumptions, f1 × g1 ≤ f2 × g2 iff f1 ≤ f2 and g1 ≤ g2.

Русский

При предположениях NeBot, f1 × g1 ≤ f2 × g2 эквивалентно f1 ≤ f2 и g1 ≤ g2.

LaTeX

$$$\bigl(\mathrm{NeBot}\, f_1\bigr)\,\bigl(\mathrm{NeBot}\, g_1\bigr) \Rightarrow (f_1 \times g_1 \le f_2 \times g_2) \iff (f_1 \le f_2) \wedge (g_1 \le g_2)$$$

Lean4

@[simp]
theorem prod_le_prod {f₁ f₂ : Filter α} {g₁ g₂ : Filter β} [NeBot f₁] [NeBot g₁] :
    f₁ ×ˢ g₁ ≤ f₂ ×ˢ g₂ ↔ f₁ ≤ f₂ ∧ g₁ ≤ g₂ :=
  ⟨fun h => ⟨map_fst_prod f₁ g₁ ▸ tendsto_fst.mono_left h, map_snd_prod f₁ g₁ ▸ tendsto_snd.mono_left h⟩, fun h =>
    prod_mono h.1 h.2⟩

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