α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : Filter α
g : Filter β
hf : Cauchy f
hg : Cauchy g
⊢ (f ×ˢ g) ×ˢ f ×ˢ g ≤ 𝓤 (α × β)
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : Filter α
g : Filter β
hf : Cauchy f
hg : Cauchy g
⊢ Cauchy (f ×ˢ g)
refine' ⟨hf.1.prod hg.1, _⟩
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : Filter α
g : Filter β
hf : Cauchy f
hg : Cauchy g
⊢ map Prod.fst (f ×ˢ g) ×ˢ map Prod.fst (f ×ˢ g) ≤ 𝓤 α ∧ map Prod.snd (f ×ˢ g) ×ˢ map Prod.snd (f ×ˢ g) ≤ 𝓤 β
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : Filter α
g : Filter β
hf : Cauchy f
hg : Cauchy g
⊢ (f ×ˢ g) ×ˢ f ×ˢ g ≤ 𝓤 (α × β)
simp only [uniformity_prod, le_inf_iff, ← map_le_iff_le_comap, ← prod_map_map_eq]
no goals
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : Filter α
g : Filter β
hf : Cauchy f
hg : Cauchy g
⊢ map Prod.fst (f ×ˢ g) ×ˢ map Prod.fst (f ×ˢ g) ≤ 𝓤 α ∧ map Prod.snd (f ×ˢ g) ×ˢ map Prod.snd (f ×ˢ g) ≤ 𝓤 β
exact
  ⟨le_trans (prod_mono tendsto_fst tendsto_fst) hf.2,
    le_trans (prod_mono tendsto_snd tendsto_snd) hg.2⟩