case intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.94197
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
ht₁ : t ∈ 𝓤 α
ht₂ : t ○ t ⊆ s
⊢ ∃ t, t ∈ 𝓤 α ∧ IsOpen t ∧ SymmetricRel t ∧ t ○ t ⊆ s
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.94197
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∃ t, t ∈ 𝓤 α ∧ IsOpen t ∧ SymmetricRel t ∧ t ○ t ⊆ s
obtain ⟨t, ht₁, ht₂⟩ := comp_mem_uniformity_sets hs
case intro.intro.intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.94197
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
ht₁ : t ∈ 𝓤 α
ht₂ : t ○ t ⊆ s
u : Set (α × α)
hu₄ : u ⊆ t
hu₁ : u ∈ 𝓤 α
hu₂ : IsOpen u
hu₃ : SymmetricRel u
⊢ ∃ t, t ∈ 𝓤 α ∧ IsOpen t ∧ SymmetricRel t ∧ t ○ t ⊆ s
case intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.94197
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
ht₁ : t ∈ 𝓤 α
ht₂ : t ○ t ⊆ s
⊢ ∃ t, t ∈ 𝓤 α ∧ IsOpen t ∧ SymmetricRel t ∧ t ○ t ⊆ s
obtain ⟨u, ⟨hu₁, hu₂, hu₃⟩, hu₄ : u ⊆ t⟩ := uniformity_hasBasis_open_symmetric.mem_iff.mp ht₁
no goals
case intro.intro.intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.94197
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
ht₁ : t ∈ 𝓤 α
ht₂ : t ○ t ⊆ s
u : Set (α × α)
hu₄ : u ⊆ t
hu₁ : u ∈ 𝓤 α
hu₂ : IsOpen u
hu₃ : SymmetricRel u
⊢ ∃ t, t ∈ 𝓤 α ∧ IsOpen t ∧ SymmetricRel t ∧ t ○ t ⊆ s
exact ⟨u, hu₁, hu₂, hu₃, (compRel_mono hu₄ hu₄).trans ht₂⟩