α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.74705
inst✝ : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed B
h : Disjoint A B
this : Bᶜ ∈ 𝓝ˢ A
⊢ ∃ V, V ∈ 𝓤 α ∧ Disjoint (⋃ (x : α) (_ : x ∈ A), ball x V) (⋃ (x : α) (_ : x ∈ B), ball x V)
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.74705
inst✝ : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed B
h : Disjoint A B
⊢ ∃ V, V ∈ 𝓤 α ∧ Disjoint (⋃ (x : α) (_ : x ∈ A), ball x V) (⋃ (x : α) (_ : x ∈ B), ball x V)
have : Bᶜ ∈ 𝓝ˢ A := hB.isOpen_compl.mem_nhdsSet.mpr h.le_compl_right
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.74705
inst✝ : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed B
h : Disjoint A B
this : ∃ i, i ∈ 𝓤 α ∧ (⋃ (x : α) (_ : x ∈ A), ball x (id i)) ⊆ Bᶜ
⊢ ∃ V, V ∈ 𝓤 α ∧ Disjoint (⋃ (x : α) (_ : x ∈ A), ball x V) (⋃ (x : α) (_ : x ∈ B), ball x V)
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.74705
inst✝ : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed B
h : Disjoint A B
this : Bᶜ ∈ 𝓝ˢ A
⊢ ∃ V, V ∈ 𝓤 α ∧ Disjoint (⋃ (x : α) (_ : x ∈ A), ball x V) (⋃ (x : α) (_ : x ∈ B), ball x V)
rw [(hA.nhdsSet_basis_uniformity (Filter.basis_sets _)).mem_iff] at this
case intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.74705
inst✝ : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed B
h : Disjoint A B
U : Set (α × α)
hU : U ∈ 𝓤 α
hUAB : (⋃ (x : α) (_ : x ∈ A), ball x (id U)) ⊆ Bᶜ
⊢ ∃ V, V ∈ 𝓤 α ∧ Disjoint (⋃ (x : α) (_ : x ∈ A), ball x V) (⋃ (x : α) (_ : x ∈ B), ball x V)
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.74705
inst✝ : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed B
h : Disjoint A B
this : ∃ i, i ∈ 𝓤 α ∧ (⋃ (x : α) (_ : x ∈ A), ball x (id i)) ⊆ Bᶜ
⊢ ∃ V, V ∈ 𝓤 α ∧ Disjoint (⋃ (x : α) (_ : x ∈ A), ball x V) (⋃ (x : α) (_ : x ∈ B), ball x V)
rcases this with ⟨U, hU, hUAB⟩
case intro.intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.74705
inst✝ : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed B
h : Disjoint A B
U : Set (α × α)
hU : U ∈ 𝓤 α
hUAB : (⋃ (x : α) (_ : x ∈ A), ball x (id U)) ⊆ Bᶜ
V : Set (α × α)
hV : V ∈ 𝓤 α
hVsymm : SymmetricRel V
hVU : V ○ V ⊆ U
⊢ ∃ V, V ∈ 𝓤 α ∧ Disjoint (⋃ (x : α) (_ : x ∈ A), ball x V) (⋃ (x : α) (_ : x ∈ B), ball x V)
case intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.74705
inst✝ : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed B
h : Disjoint A B
U : Set (α × α)
hU : U ∈ 𝓤 α
hUAB : (⋃ (x : α) (_ : x ∈ A), ball x (id U)) ⊆ Bᶜ
⊢ ∃ V, V ∈ 𝓤 α ∧ Disjoint (⋃ (x : α) (_ : x ∈ A), ball x V) (⋃ (x : α) (_ : x ∈ B), ball x V)
rcases comp_symm_mem_uniformity_sets hU with ⟨V, hV, hVsymm, hVU⟩
case intro.intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.74705
inst✝ : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed B
h : Disjoint A B
U : Set (α × α)
hU : U ∈ 𝓤 α
hUAB : (⋃ (x : α) (_ : x ∈ A), ball x (id U)) ⊆ Bᶜ
V : Set (α × α)
hV : V ∈ 𝓤 α
hVsymm : SymmetricRel V
hVU : V ○ V ⊆ U
x : α
⊢ (x ∈ ⋃ (x : α) (_ : x ∈ A), ball x V) → ¬x ∈ ⋃ (x : α) (_ : x ∈ B), ball x V
case intro.intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.74705
inst✝ : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed B
h : Disjoint A B
U : Set (α × α)
hU : U ∈ 𝓤 α
hUAB : (⋃ (x : α) (_ : x ∈ A), ball x (id U)) ⊆ Bᶜ
V : Set (α × α)
hV : V ∈ 𝓤 α
hVsymm : SymmetricRel V
hVU : V ○ V ⊆ U
⊢ ∃ V, V ∈ 𝓤 α ∧ Disjoint (⋃ (x : α) (_ : x ∈ A), ball x V) (⋃ (x : α) (_ : x ∈ B), ball x V)
refine' ⟨V, hV, Set.disjoint_left.mpr fun x => _⟩
case intro.intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.74705
inst✝ : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed B
h : Disjoint A B
U : Set (α × α)
hU : U ∈ 𝓤 α
hUAB : (⋃ (x : α) (_ : x ∈ A), ball x (id U)) ⊆ Bᶜ
V : Set (α × α)
hV : V ∈ 𝓤 α
hVsymm : SymmetricRel V
hVU : V ○ V ⊆ U
x : α
⊢ (∃ i j, x ∈ ball i V) → ¬∃ i j, x ∈ ball i V
case intro.intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.74705
inst✝ : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed B
h : Disjoint A B
U : Set (α × α)
hU : U ∈ 𝓤 α
hUAB : (⋃ (x : α) (_ : x ∈ A), ball x (id U)) ⊆ Bᶜ
V : Set (α × α)
hV : V ∈ 𝓤 α
hVsymm : SymmetricRel V
hVU : V ○ V ⊆ U
x : α
⊢ (x ∈ ⋃ (x : α) (_ : x ∈ A), ball x V) → ¬x ∈ ⋃ (x : α) (_ : x ∈ B), ball x V
simp only [mem_iUnion₂]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.74705
inst✝ : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed B
h : Disjoint A B
U : Set (α × α)
hU : U ∈ 𝓤 α
hUAB : (⋃ (x : α) (_ : x ∈ A), ball x (id U)) ⊆ Bᶜ
V : Set (α × α)
hV : V ∈ 𝓤 α
hVsymm : SymmetricRel V
hVU : V ○ V ⊆ U
x a : α
ha : a ∈ A
hxa : x ∈ ball a V
b : α
hb : b ∈ B
hxb : x ∈ ball b V
⊢ False
case intro.intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.74705
inst✝ : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed B
h : Disjoint A B
U : Set (α × α)
hU : U ∈ 𝓤 α
hUAB : (⋃ (x : α) (_ : x ∈ A), ball x (id U)) ⊆ Bᶜ
V : Set (α × α)
hV : V ∈ 𝓤 α
hVsymm : SymmetricRel V
hVU : V ○ V ⊆ U
x : α
⊢ (∃ i j, x ∈ ball i V) → ¬∃ i j, x ∈ ball i V
rintro ⟨a, ha, hxa⟩ ⟨b, hb, hxb⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.74705
inst✝ : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed B
h : Disjoint A B
U : Set (α × α)
hU : U ∈ 𝓤 α
hUAB : (⋃ (x : α) (_ : x ∈ A), ball x (id U)) ⊆ Bᶜ
V : Set (α × α)
hV : V ∈ 𝓤 α
hVsymm : SymmetricRel V
hVU : V ○ V ⊆ U
x a : α
ha : a ∈ A
hxa : a ∈ ball x V
b : α
hb : b ∈ B
hxb : b ∈ ball x V
⊢ False
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.74705
inst✝ : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed B
h : Disjoint A B
U : Set (α × α)
hU : U ∈ 𝓤 α
hUAB : (⋃ (x : α) (_ : x ∈ A), ball x (id U)) ⊆ Bᶜ
V : Set (α × α)
hV : V ∈ 𝓤 α
hVsymm : SymmetricRel V
hVU : V ○ V ⊆ U
x a : α
ha : a ∈ A
hxa : x ∈ ball a V
b : α
hb : b ∈ B
hxb : x ∈ ball b V
⊢ False
rw [mem_ball_symmetry hVsymm] at hxa hxb
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.74705
inst✝ : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed B
h : Disjoint A B
U : Set (α × α)
hU : U ∈ 𝓤 α
hUAB : (⋃ (x : α) (_ : x ∈ A), ball x (id U)) ⊆ Bᶜ
V : Set (α × α)
hV : V ∈ 𝓤 α
hVsymm : SymmetricRel V
hVU : V ○ V ⊆ U
x a : α
ha : a ∈ A
hxa : a ∈ ball x V
b : α
hb : b ∈ B
hxb : b ∈ ball x V
⊢ False
exact hUAB (mem_iUnion₂_of_mem ha <| hVU <| mem_comp_of_mem_ball hVsymm hxa hxb) hb