case h
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.55168
inst✝ : UniformSpace α
V : Set (β × β)
hV : SymmetricRel V
x y : β
⊢ y ∈ ball x V ↔ y ∈ {y | (y, x) ∈ V}
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.55168
inst✝ : UniformSpace α
V : Set (β × β)
hV : SymmetricRel V
x : β
⊢ ball x V = {y | (y, x) ∈ V}
ext y
case h
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.55168
inst✝ : UniformSpace α
V : Set (β × β)
hV : SymmetricRel V
x y : β
⊢ x ∈ ball y V ↔ y ∈ {y | (y, x) ∈ V}
case h
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.55168
inst✝ : UniformSpace α
V : Set (β × β)
hV : SymmetricRel V
x y : β
⊢ y ∈ ball x V ↔ y ∈ {y | (y, x) ∈ V}
rw [mem_ball_symmetry hV]
no goals
case h
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.55168
inst✝ : UniformSpace α
V : Set (β × β)
hV : SymmetricRel V
x y : β
⊢ x ∈ ball y V ↔ y ∈ {y | (y, x) ∈ V}
exact Iff.rfl