α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.60190
inst✝ : UniformSpace α
x : α
s : Set α
⊢ (∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s) ↔ ∃ V, V ∈ 𝓤 α ∧ SymmetricRel V ∧ ball x V ⊆ s
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.60190
inst✝ : UniformSpace α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ ∃ V, V ∈ 𝓤 α ∧ SymmetricRel V ∧ ball x V ⊆ s
rw [UniformSpace.mem_nhds_iff]
case mp
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.60190
inst✝ : UniformSpace α
x : α
s : Set α
⊢ (∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s) → ∃ V, V ∈ 𝓤 α ∧ SymmetricRel V ∧ ball x V ⊆ s

case mpr
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.60190
inst✝ : UniformSpace α
x : α
s : Set α
⊢ (∃ V, V ∈ 𝓤 α ∧ SymmetricRel V ∧ ball x V ⊆ s) → ∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.60190
inst✝ : UniformSpace α
x : α
s : Set α
⊢ (∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s) ↔ ∃ V, V ∈ 𝓤 α ∧ SymmetricRel V ∧ ball x V ⊆ s
constructor
case mp.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.60190
inst✝ : UniformSpace α
x : α
s : Set α
V : Set (α × α)
V_in : V ∈ 𝓤 α
V_sub : ball x V ⊆ s
⊢ ∃ V, V ∈ 𝓤 α ∧ SymmetricRel V ∧ ball x V ⊆ s
case mp
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.60190
inst✝ : UniformSpace α
x : α
s : Set α
⊢ (∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s) → ∃ V, V ∈ 𝓤 α ∧ SymmetricRel V ∧ ball x V ⊆ s
rintro ⟨V, V_in, V_sub⟩
case mp.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.60190
inst✝ : UniformSpace α
x : α
s : Set α
V : Set (α × α)
V_in : V ∈ 𝓤 α
V_sub : ball x V ⊆ s
⊢ ball x (symmetrizeRel V) ⊆ s
case mp.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.60190
inst✝ : UniformSpace α
x : α
s : Set α
V : Set (α × α)
V_in : V ∈ 𝓤 α
V_sub : ball x V ⊆ s
⊢ ∃ V, V ∈ 𝓤 α ∧ SymmetricRel V ∧ ball x V ⊆ s
use symmetrizeRel V, symmetrize_mem_uniformity V_in, symmetric_symmetrizeRel V
no goals
case mp.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.60190
inst✝ : UniformSpace α
x : α
s : Set α
V : Set (α × α)
V_in : V ∈ 𝓤 α
V_sub : ball x V ⊆ s
⊢ ball x (symmetrizeRel V) ⊆ s
exact Subset.trans (ball_mono (symmetrizeRel_subset_self V) x) V_sub
case mpr.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.60190
inst✝ : UniformSpace α
x : α
s : Set α
V : Set (α × α)
V_in : V ∈ 𝓤 α
left✝ : SymmetricRel V
V_sub : ball x V ⊆ s
⊢ ∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s
case mpr
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.60190
inst✝ : UniformSpace α
x : α
s : Set α
⊢ (∃ V, V ∈ 𝓤 α ∧ SymmetricRel V ∧ ball x V ⊆ s) → ∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s
rintro ⟨V, V_in, _, V_sub⟩
no goals
case mpr.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.60190
inst✝ : UniformSpace α
x : α
s : Set α
V : Set (α × α)
V_in : V ∈ 𝓤 α
left✝ : SymmetricRel V
V_sub : ball x V ⊆ s
⊢ ∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s
exact ⟨V, V_in, V_sub⟩