case h
α : Type u
β : Type v
X : Type ?u.398898
ι : Type ?u.398901
inst✝² : PseudoMetricSpace α
π : β → Type u_1
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x : (b : β) → π b
r : ℝ
hr : 0 < r
p : (b : β) → π b
⊢ p ∈ ball x r ↔ p ∈ Set.pi Set.univ fun b => ball (x b) r
α : Type u
β : Type v
X : Type ?u.398898
ι : Type ?u.398901
inst✝² : PseudoMetricSpace α
π : β → Type u_1
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x : (b : β) → π b
r : ℝ
hr : 0 < r
⊢ ball x r = Set.pi Set.univ fun b => ball (x b) r
ext p
no goals
case h
α : Type u
β : Type v
X : Type ?u.398898
ι : Type ?u.398901
inst✝² : PseudoMetricSpace α
π : β → Type u_1
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x : (b : β) → π b
r : ℝ
hr : 0 < r
p : (b : β) → π b
⊢ p ∈ ball x r ↔ p ∈ Set.pi Set.univ fun b => ball (x b) r
simp [dist_pi_lt_iff hr]