case intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
hU : HasBasis (𝓤 α) p s
A B : Set α
hA : IsCompact A
hB : IsClosed B
h : Disjoint A B
V : Set (α × α)
hV : V ∈ 𝓤 α
hVAB : Disjoint (⋃ (x : α) (_ : x ∈ A), ball x V) (⋃ (x : α) (_ : x ∈ B), ball x V)
⊢ ∃ i, p i ∧ Disjoint (⋃ (x : α) (_ : x ∈ A), ball x (s i)) (⋃ (x : α) (_ : x ∈ B), ball x (s i))
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
hU : HasBasis (𝓤 α) p s
A B : Set α
hA : IsCompact A
hB : IsClosed B
h : Disjoint A B
⊢ ∃ i, p i ∧ Disjoint (⋃ (x : α) (_ : x ∈ A), ball x (s i)) (⋃ (x : α) (_ : x ∈ B), ball x (s i))
rcases h.exists_uniform_thickening hA hB with ⟨V, hV, hVAB⟩
case intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
hU : HasBasis (𝓤 α) p s
A B : Set α
hA : IsCompact A
hB : IsClosed B
h : Disjoint A B
V : Set (α × α)
hV : V ∈ 𝓤 α
hVAB : Disjoint (⋃ (x : α) (_ : x ∈ A), ball x V) (⋃ (x : α) (_ : x ∈ B), ball x V)
i : ι
hi : p i
hiV : s i ⊆ V
⊢ ∃ i, p i ∧ Disjoint (⋃ (x : α) (_ : x ∈ A), ball x (s i)) (⋃ (x : α) (_ : x ∈ B), ball x (s i))
case intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
hU : HasBasis (𝓤 α) p s
A B : Set α
hA : IsCompact A
hB : IsClosed B
h : Disjoint A B
V : Set (α × α)
hV : V ∈ 𝓤 α
hVAB : Disjoint (⋃ (x : α) (_ : x ∈ A), ball x V) (⋃ (x : α) (_ : x ∈ B), ball x V)
⊢ ∃ i, p i ∧ Disjoint (⋃ (x : α) (_ : x ∈ A), ball x (s i)) (⋃ (x : α) (_ : x ∈ B), ball x (s i))
rcases hU.mem_iff.1 hV with ⟨i, hi, hiV⟩
no goals
case intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
hU : HasBasis (𝓤 α) p s
A B : Set α
hA : IsCompact A
hB : IsClosed B
h : Disjoint A B
V : Set (α × α)
hV : V ∈ 𝓤 α
hVAB : Disjoint (⋃ (x : α) (_ : x ∈ A), ball x V) (⋃ (x : α) (_ : x ∈ B), ball x V)
i : ι
hi : p i
hiV : s i ⊆ V
⊢ ∃ i, p i ∧ Disjoint (⋃ (x : α) (_ : x ∈ A), ball x (s i)) (⋃ (x : α) (_ : x ∈ B), ball x (s i))
exact ⟨i, hi, hVAB.mono (iUnion₂_mono fun a _ => ball_mono hiV a)
  (iUnion₂_mono fun b _ => ball_mono hiV b)⟩