X : Type u_2
inst✝ : EMetricSpace X
s✝ t✝ : Set X
x y : X
ι : Type u_1
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
X : Type u_2
inst✝ : EMetricSpace X
s✝ t✝ : Set X
x y : X
ι : Type u_1
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
refine' Finite.induction_on hI (by simp) @fun i I _ _ hI => _
no goals
X : Type u_2
inst✝ : EMetricSpace X
s✝ t✝ : Set X
x y : X
ι : Type u_1
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
rw [biUnion_insert, ball_insert_iff, union_left_iff, hI]
no goals
X : Type u_2
inst✝ : EMetricSpace X
s✝ t✝ : Set X
x y : X
ι : Type u_1
I : Set ι
hI : Set.Finite I
s : ι → Set X
t : Set X
⊢ IsMetricSeparated (⋃ (i : ι) (_ : i ∈ ∅), s i) t ↔ ∀ (i : ι), i ∈ ∅ → IsMetricSeparated (s i) t
simp