[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
⊢ AntilipschitzWith K f ↔ ∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)
[PROOFSTEP]
simp only [AntilipschitzWith, edist_nndist]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
⊢ (∀ (x y : α), ↑(nndist x y) ≤ ↑K * ↑(nndist (f x) (f y))) ↔ ∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
⊢ AntilipschitzWith K f ↔ ∀ (x y : α), dist x y ≤ ↑K * dist (f x) (f y)
[PROOFSTEP]
simp only [antilipschitzWith_iff_le_mul_nndist, dist_nndist]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
⊢ (∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)) ↔ ∀ (x y : α), ↑(nndist x y) ≤ ↑K * ↑(nndist (f x) (f y))
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x y : α
⊢ K⁻¹ * nndist x y ≤ nndist (f x) (f y)
[PROOFSTEP]
simpa only [div_eq_inv_mul] using NNReal.div_le_of_le_mul' (hf.le_mul_nndist x y)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x y : α
⊢ ↑K⁻¹ * dist x y ≤ dist (f x) (f y)
[PROOFSTEP]
exact_mod_cast hf.mul_le_nndist x y
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
inst✝⁴ : PseudoEMetricSpace α✝
inst✝³ : PseudoEMetricSpace β✝
inst✝² : PseudoEMetricSpace γ
K✝ : ℝ≥0
f✝ : α✝ → β✝
α : Type u_4
β : Type u_5
inst✝¹ : EMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x y : α
h : f x = f y
⊢ x = y
[PROOFSTEP]
simpa only [h, edist_self, mul_zero, edist_le_zero] using hf x y
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x y : α
⊢ (↑K)⁻¹ * edist x y ≤ edist (f x) (f y)
[PROOFSTEP]
rw [mul_comm, ← div_eq_mul_inv]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x y : α
⊢ edist x y / ↑K ≤ edist (f x) (f y)
[PROOFSTEP]
exact ENNReal.div_le_of_le_mul' (hf x y)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
x y : α
⊢ edist x y ≤ ↑1 * edist (id x) (id y)
[PROOFSTEP]
simp only [ENNReal.coe_one, one_mul, id, le_refl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f✝ : α → β
Kg : ℝ≥0
g : β → γ
hg : AntilipschitzWith Kg g
Kf : ℝ≥0
f : α → β
hf : AntilipschitzWith Kf f
x y : α
⊢ ↑Kf * (↑Kg * edist (g (f x)) (g (f y))) = ↑(Kf * Kg) * edist ((g ∘ f) x) ((g ∘ f) y)
[PROOFSTEP]
rw [ENNReal.coe_mul, mul_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f✝ : α → β
Kg : ℝ≥0
g : β → γ
hg : AntilipschitzWith Kg g
Kf : ℝ≥0
f : α → β
hf : AntilipschitzWith Kf f
x y : α
⊢ ↑Kf * (↑Kg * edist (g (f x)) (g (f y))) = ↑Kf * (↑Kg * edist ((g ∘ f) x) ((g ∘ f) y))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
s : Set α
hf : AntilipschitzWith K (Set.restrict s f)
g : β → α
t : Set β
g_maps : MapsTo g t s
g_inv : RightInvOn g f t
x y : ↑t
⊢ edist (Set.restrict t g x) (Set.restrict t g y) ≤ ↑K * edist x y
[PROOFSTEP]
simpa only [restrict_apply, g_inv x.mem, g_inv y.mem, Subtype.edist_eq, Subtype.coe_mk] using
  hf ⟨g x, g_maps x.mem⟩ ⟨g y, g_maps y.mem⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
g : β → α
hg : Function.RightInverse g f
⊢ LipschitzWith K g
[PROOFSTEP]
intro x y
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
g : β → α
hg : Function.RightInverse g f
x y : β
⊢ edist (g x) (g y) ≤ ↑K * edist x y
[PROOFSTEP]
have := hf (g x) (g y)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
g : β → α
hg : Function.RightInverse g f
x y : β
this : edist (g x) (g y) ≤ ↑K * edist (f (g x)) (f (g y))
⊢ edist (g x) (g y) ≤ ↑K * edist x y
[PROOFSTEP]
rwa [hg x, hg y] at this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
⊢ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
[PROOFSTEP]
refine ((uniformity_basis_edist.comap _).le_basis_iff uniformity_basis_edist).2 fun ε h₀ => ?_
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
ε : ℝ≥0∞
h₀ : 0 < ε
⊢ ∃ i, 0 < i ∧ Prod.map f f ⁻¹' {p | edist p.fst p.snd < i} ⊆ {p | edist p.fst p.snd < ε}
[PROOFSTEP]
refine ⟨(↑K)⁻¹ * ε, ENNReal.mul_pos (ENNReal.inv_ne_zero.2 ENNReal.coe_ne_top) h₀.ne', ?_⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
ε : ℝ≥0∞
h₀ : 0 < ε
⊢ Prod.map f f ⁻¹' {p | edist p.fst p.snd < (↑K)⁻¹ * ε} ⊆ {p | edist p.fst p.snd < ε}
[PROOFSTEP]
refine' fun x hx => (hf x.1 x.2).trans_lt _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
ε : ℝ≥0∞
h₀ : 0 < ε
x : α × α
hx : x ∈ Prod.map f f ⁻¹' {p | edist p.fst p.snd < (↑K)⁻¹ * ε}
⊢ ↑K * edist (f x.fst) (f x.snd) < ε
[PROOFSTEP]
rw [mul_comm, ← div_eq_mul_inv] at hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
ε : ℝ≥0∞
h₀ : 0 < ε
x : α × α
hx : x ∈ Prod.map f f ⁻¹' {p | edist p.fst p.snd < ε / ↑K}
⊢ ↑K * edist (f x.fst) (f x.snd) < ε
[PROOFSTEP]
rw [mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
ε : ℝ≥0∞
h₀ : 0 < ε
x : α × α
hx : x ∈ Prod.map f f ⁻¹' {p | edist p.fst p.snd < ε / ↑K}
⊢ edist (f x.fst) (f x.snd) * ↑K < ε
[PROOFSTEP]
exact ENNReal.mul_lt_of_lt_div hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : PseudoEMetricSpace γ
K✝ : ℝ≥0
f : α → β
inst✝ : Subsingleton α
K : ℝ≥0
x y : α
⊢ edist x y ≤ ↑K * edist (f x) (f y)
[PROOFSTEP]
simp only [Subsingleton.elim x y, edist_self, zero_le]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
s : Set β
hs : Metric.Bounded s
x : α
hx : x ∈ f ⁻¹' s
y : α
hy : y ∈ f ⁻¹' s
⊢ ↑K * dist (f x) (f y) ≤ ↑K * diam s
[PROOFSTEP]
gcongr
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
s : Set β
hs : Metric.Bounded s
x : α
hx : x ∈ f ⁻¹' s
y : α
hy : y ∈ f ⁻¹' s
⊢ dist (f x) (f y) ≤ diam s
[PROOFSTEP]
exact dist_le_diam_of_mem hs hx hy
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : PseudoMetricSpace α✝
inst✝² : PseudoMetricSpace β
K✝ : ℝ≥0
f✝ : α✝ → β
α : Type u_4
inst✝¹ : MetricSpace α
K : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K f
f_cont : Continuous f
hf : Function.Surjective f
⊢ ProperSpace β
[PROOFSTEP]
refine ⟨fun x₀ r => ?_⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : PseudoMetricSpace α✝
inst✝² : PseudoMetricSpace β
K✝ : ℝ≥0
f✝ : α✝ → β
α : Type u_4
inst✝¹ : MetricSpace α
K : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K f
f_cont : Continuous f
hf : Function.Surjective f
x₀ : β
r : ℝ
⊢ IsCompact (closedBall x₀ r)
[PROOFSTEP]
let K := f ⁻¹' closedBall x₀ r
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : PseudoMetricSpace α✝
inst✝² : PseudoMetricSpace β
K✝¹ : ℝ≥0
f✝ : α✝ → β
α : Type u_4
inst✝¹ : MetricSpace α
K✝ : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K✝ f
f_cont : Continuous f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
⊢ IsCompact (closedBall x₀ r)
[PROOFSTEP]
have A : IsClosed K := isClosed_ball.preimage f_cont
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : PseudoMetricSpace α✝
inst✝² : PseudoMetricSpace β
K✝¹ : ℝ≥0
f✝ : α✝ → β
α : Type u_4
inst✝¹ : MetricSpace α
K✝ : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K✝ f
f_cont : Continuous f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
A : IsClosed K
⊢ IsCompact (closedBall x₀ r)
[PROOFSTEP]
have B : Bounded K := hK.bounded_preimage bounded_closedBall
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : PseudoMetricSpace α✝
inst✝² : PseudoMetricSpace β
K✝¹ : ℝ≥0
f✝ : α✝ → β
α : Type u_4
inst✝¹ : MetricSpace α
K✝ : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K✝ f
f_cont : Continuous f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
A : IsClosed K
B : Metric.Bounded K
⊢ IsCompact (closedBall x₀ r)
[PROOFSTEP]
have : IsCompact K := isCompact_iff_isClosed_bounded.2 ⟨A, B⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : PseudoMetricSpace α✝
inst✝² : PseudoMetricSpace β
K✝¹ : ℝ≥0
f✝ : α✝ → β
α : Type u_4
inst✝¹ : MetricSpace α
K✝ : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K✝ f
f_cont : Continuous f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
A : IsClosed K
B : Metric.Bounded K
this : IsCompact K
⊢ IsCompact (closedBall x₀ r)
[PROOFSTEP]
convert this.image f_cont
[GOAL]
case h.e'_3
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : PseudoMetricSpace α✝
inst✝² : PseudoMetricSpace β
K✝¹ : ℝ≥0
f✝ : α✝ → β
α : Type u_4
inst✝¹ : MetricSpace α
K✝ : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K✝ f
f_cont : Continuous f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
A : IsClosed K
B : Metric.Bounded K
this : IsCompact K
⊢ closedBall x₀ r = f '' K
[PROOFSTEP]
exact (hf.image_preimage _).symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
g : β → α
hg : Function.RightInverse g f
x y : β
⊢ edist x y ≤ ↑K * edist (g x) (g y)
[PROOFSTEP]
simpa only [hg _] using hf (g x) (g y)


[GOAL]
X : Type u_1
inst✝ : EMetricSpace X
s t : Set X
x✝ y : X
h : IsMetricSeparated s t
r : ENNReal
r0 : r ≠ 0
hr : ∀ (x : X), x ∈ s → ∀ (y : X), y ∈ t → r ≤ edist x y
x : X
hx1 : x ∈ s
hx2 : x ∈ t
⊢ r = 0
[PROOFSTEP]
simpa using hr x hx1 x hx2
[GOAL]
X : Type u_1
inst✝ : EMetricSpace X
s t : Set X
x y : X
s' : Set X
h : IsMetricSeparated s t
h' : IsMetricSeparated s' t
⊢ IsMetricSeparated (s ∪ s') t
[PROOFSTEP]
rcases h, h' with ⟨⟨r, r0, hr⟩, ⟨r', r0', hr'⟩⟩
[GOAL]
case intro.intro.intro.intro
X : Type u_1
inst✝ : EMetricSpace X
s t : Set X
x y : X
s' : Set X
r : ENNReal
r0 : r ≠ 0
hr : ∀ (x : X), x ∈ s → ∀ (y : X), y ∈ t → r ≤ edist x y
r' : ENNReal
r0' : r' ≠ 0
hr' : ∀ (x : X), x ∈ s' → ∀ (y : X), y ∈ t → r' ≤ edist x y
⊢ IsMetricSeparated (s ∪ s') t
[PROOFSTEP]
refine' ⟨min r r', _, fun x hx y hy => hx.elim _ _⟩
[GOAL]
case intro.intro.intro.intro.refine'_1
X : Type u_1
inst✝ : EMetricSpace X
s t : Set X
x y : X
s' : Set X
r : ENNReal
r0 : r ≠ 0
hr : ∀ (x : X), x ∈ s → ∀ (y : X), y ∈ t → r ≤ edist x y
r' : ENNReal
r0' : r' ≠ 0
hr' : ∀ (x : X), x ∈ s' → ∀ (y : X), y ∈ t → r' ≤ edist x y
⊢ min r r' ≠ 0
[PROOFSTEP]
rw [← pos_iff_ne_zero] at r0 r0' ⊢
[GOAL]
case intro.intro.intro.intro.refine'_1
X : Type u_1
inst✝ : EMetricSpace X
s t : Set X
x y : X
s' : Set X
r : ENNReal
r0 : 0 < r
hr : ∀ (x : X), x ∈ s → ∀ (y : X), y ∈ t → r ≤ edist x y
r' : ENNReal
r0' : 0 < r'
hr' : ∀ (x : X), x ∈ s' → ∀ (y : X), y ∈ t → r' ≤ edist x y
⊢ 0 < min r r'
[PROOFSTEP]
exact lt_min r0 r0'
[GOAL]
case intro.intro.intro.intro.refine'_2
X : Type u_1
inst✝ : EMetricSpace X
s t : Set X
x✝ y✝ : X
s' : Set X
r : ENNReal
r0 : r ≠ 0
hr : ∀ (x : X), x ∈ s → ∀ (y : X), y ∈ t → r ≤ edist x y
r' : ENNReal
r0' : r' ≠ 0
hr' : ∀ (x : X), x ∈ s' → ∀ (y : X), y ∈ t → r' ≤ edist x y
x : X
hx : x ∈ s ∪ s'
y : X
hy : y ∈ t
⊢ x ∈ s → min r r' ≤ edist x y
[PROOFSTEP]
exact fun hx => (min_le_left _ _).trans (hr _ hx _ hy)
[GOAL]
case intro.intro.intro.intro.refine'_3
X : Type u_1
inst✝ : EMetricSpace X
s t : Set X
x✝ y✝ : X
s' : Set X
r : ENNReal
r0 : r ≠ 0
hr : ∀ (x : X), x ∈ s → ∀ (y : X), y ∈ t → r ≤ edist x y
r' : ENNReal
r0' : r' ≠ 0
hr' : ∀ (x : X), x ∈ s' → ∀ (y : X), y ∈ t → r' ≤ edist x y
x : X
hx : x ∈ s ∪ s'
y : X
hy : y ∈ t
⊢ x ∈ s' → min r r' ≤ edist x y
[PROOFSTEP]
exact fun hx => (min_le_right _ _).trans (hr' _ hx _ hy)
[GOAL]
X : Type u_1
inst✝ : EMetricSpace X
s✝ t✝ : Set X
x y : X
ι : Type u_2
I : Set ι
hI : Set.Finite I
s : ι → Set X
t : Set X
⊢ IsMetricSeparated (⋃ (i : ι) (_ : i ∈ I), s i) t ↔ ∀ (i : ι), i ∈ I → IsMetricSeparated (s i) t
[PROOFSTEP]
refine' Finite.induction_on hI (by simp) @fun i I _ _ hI => _
[GOAL]
X : Type u_1
inst✝ : EMetricSpace X
s✝ t✝ : Set X
x y : X
ι : Type u_2
I : Set ι
hI : Set.Finite I
s : ι → Set X
t : Set X
⊢ IsMetricSeparated (⋃ (i : ι) (_ : i ∈ ∅), s i) t ↔ ∀ (i : ι), i ∈ ∅ → IsMetricSeparated (s i) t
[PROOFSTEP]
simp
[GOAL]
X : Type u_1
inst✝ : EMetricSpace X
s✝ t✝ : Set X
x y : X
ι : Type u_2
I✝ : Set ι
hI✝ : Set.Finite I✝
s : ι → Set X
t : Set X
i : ι
I : Set ι
x✝¹ : ¬i ∈ I
x✝ : Set.Finite I
hI : IsMetricSeparated (⋃ (i : ι) (_ : i ∈ I), s i) t ↔ ∀ (i : ι), i ∈ I → IsMetricSeparated (s i) t
⊢ IsMetricSeparated (⋃ (i_1 : ι) (_ : i_1 ∈ insert i I), s i_1) t ↔
    ∀ (i_1 : ι), i_1 ∈ insert i I → IsMetricSeparated (s i_1) t
[PROOFSTEP]
rw [biUnion_insert, ball_insert_iff, union_left_iff, hI]
[GOAL]
X : Type u_1
inst✝ : EMetricSpace X
s✝ t✝ : Set X
x y : X
ι : Type u_2
I : Set ι
hI : Set.Finite I
s : Set X
t : ι → Set X
⊢ IsMetricSeparated s (⋃ (i : ι) (_ : i ∈ I), t i) ↔ ∀ (i : ι), i ∈ I → IsMetricSeparated s (t i)
[PROOFSTEP]
simpa only [@comm _ _ s] using finite_iUnion_left_iff hI