[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
