α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s : Set (CauchyFilter α × CauchyFilter α)
t : Set (α × α)
_h : t ∈ 𝓤 α
⊢ gen t ⊆ s ↔ ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s : Set (CauchyFilter α × CauchyFilter α)
⊢ s ∈ 𝓤 (CauchyFilter α) ↔ ∃ t, t ∈ 𝓤 α ∧ ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s
refine mem_uniformity.trans (exists_congr (fun t => and_congr_right_iff.mpr (fun _h => ?_)))
no goals
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s : Set (CauchyFilter α × CauchyFilter α)
t : Set (α × α)
_h : t ∈ 𝓤 α
⊢ gen t ⊆ s ↔ ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s
exact ⟨fun h _f _g ht => h ht, fun h _p hp => h _ _ hp⟩