[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
s : Set (α × α)
⊢ idRel ⊆ s ↔ ∀ (a : α), (a, a) ∈ s
[PROOFSTEP]
simp [subset_def]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
x✝ : α × α
a b : α
⊢ (a, b) ∈ Prod.swap '' idRel ↔ (a, b) ∈ idRel
[PROOFSTEP]
simpa [image_swap_eq_preimage_swap] using eq_comm
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
r : Set (α × α)
x✝ : α × α
a b : α
⊢ (a, b) ∈ idRel ○ r ↔ (a, b) ∈ r
[PROOFSTEP]
simp
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
r s t : Set (α × α)
⊢ r ○ s ○ t = r ○ (s ○ t)
[PROOFSTEP]
ext ⟨a, b⟩
[GOAL]
case h.mk
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
r s t : Set (α × α)
a b : α
⊢ (a, b) ∈ r ○ s ○ t ↔ (a, b) ∈ r ○ (s ○ t)
[PROOFSTEP]
simp only [mem_compRel]
[GOAL]
case h.mk
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
r s t : Set (α × α)
a b : α
⊢ (∃ z, (∃ z_1, (a, z_1) ∈ r ∧ (z_1, z) ∈ s) ∧ (z, b) ∈ t) ↔ ∃ z, (a, z) ∈ r ∧ ∃ z_1, (z, z_1) ∈ s ∧ (z_1, b) ∈ t
[PROOFSTEP]
tauto
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
s t : Set (α × α)
h : idRel ⊆ s
n : ℕ
⊢ t ⊆ (fun x => s ○ x)^[n] t
[PROOFSTEP]
induction' n with n ihn generalizing t
[GOAL]
case zero
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
s t✝ : Set (α × α)
h : idRel ⊆ s
t : Set (α × α)
⊢ t ⊆ (fun x => s ○ x)^[Nat.zero] t
case succ
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
s t✝ : Set (α × α)
h : idRel ⊆ s
n : ℕ
ihn : ∀ {t : Set (α × α)}, t ⊆ (fun x => s ○ x)^[n] t
t : Set (α × α)
⊢ t ⊆ (fun x => s ○ x)^[Nat.succ n] t
[PROOFSTEP]
exacts [Subset.rfl, (right_subset_compRel h).trans ihn]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
V : Set (α × α)
⊢ SymmetricRel (symmetrizeRel V)
[PROOFSTEP]
simp [SymmetricRel, symmetrizeRel, preimage_inter, inter_comm, ← preimage_comp]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
U V : Set (α × α)
hU : SymmetricRel U
hV : SymmetricRel V
⊢ SymmetricRel (U ∩ V)
[PROOFSTEP]
rw [SymmetricRel, preimage_inter, hU.eq, hV.eq]
[GOAL]
α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
α : Type u
u : Core α
⊢ (fun s => ∀ (x : α), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ u.uniformity) univ
[PROOFSTEP]
simp
[GOAL]
α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
α : Type u
u : Core α
s t : Set α
hs : (fun s => ∀ (x : α), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ u.uniformity) s
ht : (fun s => ∀ (x : α), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ u.uniformity) t
x : α
x✝ : x ∈ s ∩ t
xs : x ∈ s
xt : x ∈ t
⊢ {p | p.fst = x → p.snd ∈ s ∩ t} ∈ u.uniformity
[PROOFSTEP]
filter_upwards [hs x xs, ht x xt] with x hxs hxt hx using ⟨hxs hx, hxt hx⟩
[GOAL]
α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
α : Type u
u : Core α
s : Set (Set α)
hs : ∀ (t : Set α), t ∈ s → (fun s => ∀ (x : α), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ u.uniformity) t
x : α
x✝ : x ∈ ⋃₀ s
t : Set α
ts : t ∈ s
xt : x ∈ t
⊢ {p | p.fst = x → p.snd ∈ ⋃₀ s} ∈ u.uniformity
[PROOFSTEP]
filter_upwards [hs t ts x xt] with p ph h using ⟨t, ts, ph h⟩
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
u✝ : Core α
t : TopologicalSpace α
h : ∀ (x : α), 𝓝 x = comap (Prod.mk x) u✝.uniformity
u : Set α
⊢ IsOpen u ↔ ∀ (x : α), x ∈ u → {p | p.fst = x → p.snd ∈ u} ∈ u✝.uniformity
[PROOFSTEP]
simp only [isOpen_iff_mem_nhds, h, mem_comap_prod_mk]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
t₁ : TopologicalSpace α
u₁ : UniformSpace.Core α
o₁ : ∀ (s : Set α), IsOpen s ↔ ∀ (x : α), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ u₁.uniformity
t₂ : TopologicalSpace α
u₂ : UniformSpace.Core α
o₂ : ∀ (s : Set α), IsOpen s ↔ ∀ (x : α), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ u₂.uniformity
h : uniformity α = uniformity α
⊢ UniformSpace.mk' t₁ u₁ o₁ = UniformSpace.mk' t₂ u₂ o₂
[PROOFSTEP]
obtain rfl : u₁ = u₂ := UniformSpace.core_eq h
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
t₁ : TopologicalSpace α
u₁ : UniformSpace.Core α
o₁ : ∀ (s : Set α), IsOpen s ↔ ∀ (x : α), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ u₁.uniformity
t₂ : TopologicalSpace α
o₂ : ∀ (s : Set α), IsOpen s ↔ ∀ (x : α), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ u₁.uniformity
h : uniformity α = uniformity α
⊢ UniformSpace.mk' t₁ u₁ o₁ = UniformSpace.mk' t₂ u₁ o₂
[PROOFSTEP]
obtain rfl : t₁ = t₂ := topologicalSpace_eq <| funext fun s => by rw [o₁, o₂]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
t₁ : TopologicalSpace α
u₁ : UniformSpace.Core α
o₁ : ∀ (s : Set α), IsOpen s ↔ ∀ (x : α), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ u₁.uniformity
t₂ : TopologicalSpace α
o₂ : ∀ (s : Set α), IsOpen s ↔ ∀ (x : α), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ u₁.uniformity
h : uniformity α = uniformity α
s : Set α
⊢ IsOpen s = IsOpen s
[PROOFSTEP]
rw [o₁, o₂]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
t₁ : TopologicalSpace α
u₁ : UniformSpace.Core α
o₁ o₂ : ∀ (s : Set α), IsOpen s ↔ ∀ (x : α), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ u₁.uniformity
h : uniformity α = uniformity α
⊢ UniformSpace.mk' t₁ u₁ o₁ = UniformSpace.mk' t₁ u₁ o₂
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type ua
β✝ : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
α : Type u
β : Type v
inst✝ : OrderedAddCommMonoid β
d : α → α → β
refl : ∀ (x : α), d x x = 0
symm : ∀ (x y : α), d x y = d y x
triangle : ∀ (x y z : α), d x z ≤ d x y + d y z
half : ∀ (ε : β), ε > 0 → ∃ δ, δ > 0 ∧ ∀ (x : β), x < δ → ∀ (y : β), y < δ → x + y < ε
r : β
hr : r > 0
x : α
⊢ (x, x) ∈ {x | d x.fst x.snd < r}
[PROOFSTEP]
simpa [refl]
[GOAL]
α✝ : Type ua
β✝ : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
α : Type u
β : Type v
inst✝ : OrderedAddCommMonoid β
d : α → α → β
refl : ∀ (x : α), d x x = 0
symm : ∀ (x y : α), d x y = d y x
triangle : ∀ (x y z : α), d x z ≤ d x y + d y z
half : ∀ (ε : β), ε > 0 → ∃ δ, δ > 0 ∧ ∀ (x : β), x < δ → ∀ (y : β), y < δ → x + y < ε
r : β
x✝ : r > 0
x : α × α
hx : x ∈ {x | d x.fst x.snd < r}
⊢ Prod.swap x ∈ {x | d x.fst x.snd < r}
[PROOFSTEP]
rwa [mem_setOf, symm]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
n : ℕ
⊢ ∀ᶠ (t : Set (α × α)) in smallSets (𝓤 α), (fun x => t ○ x)^[n] t ⊆ s
[PROOFSTEP]
suffices ∀ᶠ t in (𝓤 α).smallSets, t ⊆ s ∧ (t ○ ·)^[n] t ⊆ s from (eventually_and.1 this).2
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
n : ℕ
⊢ ∀ᶠ (t : Set (α × α)) in smallSets (𝓤 α), t ⊆ s ∧ (fun x => t ○ x)^[n] t ⊆ s
[PROOFSTEP]
induction' n with n ihn generalizing s
[GOAL]
case zero
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s✝ : Set (α × α)
hs✝ : s✝ ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∀ᶠ (t : Set (α × α)) in smallSets (𝓤 α), t ⊆ s ∧ (fun x => t ○ x)^[Nat.zero] t ⊆ s
[PROOFSTEP]
simpa
[GOAL]
case succ
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s✝ : Set (α × α)
hs✝ : s✝ ∈ 𝓤 α
n : ℕ
ihn : ∀ {s : Set (α × α)}, s ∈ 𝓤 α → ∀ᶠ (t : Set (α × α)) in smallSets (𝓤 α), t ⊆ s ∧ (fun x => t ○ x)^[n] t ⊆ s
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∀ᶠ (t : Set (α × α)) in smallSets (𝓤 α), t ⊆ s ∧ (fun x => t ○ x)^[Nat.succ n] t ⊆ s
[PROOFSTEP]
rcases comp_mem_uniformity_sets hs with ⟨t, htU, hts⟩
[GOAL]
case succ.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s✝ : Set (α × α)
hs✝ : s✝ ∈ 𝓤 α
n : ℕ
ihn : ∀ {s : Set (α × α)}, s ∈ 𝓤 α → ∀ᶠ (t : Set (α × α)) in smallSets (𝓤 α), t ⊆ s ∧ (fun x => t ○ x)^[n] t ⊆ s
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
htU : t ∈ 𝓤 α
hts : t ○ t ⊆ s
⊢ ∀ᶠ (t : Set (α × α)) in smallSets (𝓤 α), t ⊆ s ∧ (fun x => t ○ x)^[Nat.succ n] t ⊆ s
[PROOFSTEP]
refine' (ihn htU).mono fun U hU => _
[GOAL]
case succ.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s✝ : Set (α × α)
hs✝ : s✝ ∈ 𝓤 α
n : ℕ
ihn : ∀ {s : Set (α × α)}, s ∈ 𝓤 α → ∀ᶠ (t : Set (α × α)) in smallSets (𝓤 α), t ⊆ s ∧ (fun x => t ○ x)^[n] t ⊆ s
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
htU : t ∈ 𝓤 α
hts : t ○ t ⊆ s
U : Set (α × α)
hU : U ⊆ t ∧ (fun x => U ○ x)^[n] U ⊆ t
⊢ U ⊆ s ∧ (fun x => U ○ x)^[Nat.succ n] U ⊆ s
[PROOFSTEP]
rw [Function.iterate_succ_apply']
[GOAL]
case succ.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s✝ : Set (α × α)
hs✝ : s✝ ∈ 𝓤 α
n : ℕ
ihn : ∀ {s : Set (α × α)}, s ∈ 𝓤 α → ∀ᶠ (t : Set (α × α)) in smallSets (𝓤 α), t ⊆ s ∧ (fun x => t ○ x)^[n] t ⊆ s
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
htU : t ∈ 𝓤 α
hts : t ○ t ⊆ s
U : Set (α × α)
hU : U ⊆ t ∧ (fun x => U ○ x)^[n] U ⊆ t
⊢ U ⊆ s ∧ U ○ (fun x => U ○ x)^[n] U ⊆ s
[PROOFSTEP]
exact ⟨hU.1.trans <| (subset_comp_self <| refl_le_uniformity htU).trans hts, (compRel_mono hU.1 hU.2).trans hts⟩
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
l : Filter β
f₁ f₂ f₃ : β → α
h₁₂ : Tendsto (fun x => (f₁ x, f₂ x)) l (𝓤 α)
h₂₃ : Tendsto (fun x => (f₂ x, f₃ x)) l (𝓤 α)
⊢ Tendsto (fun x => (f₁ x, f₃ x)) l (𝓤 α)
[PROOFSTEP]
refine' le_trans (le_lift'.2 fun s hs => mem_map.2 _) comp_le_uniformity
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
l : Filter β
f₁ f₂ f₃ : β → α
h₁₂ : Tendsto (fun x => (f₁ x, f₂ x)) l (𝓤 α)
h₂₃ : Tendsto (fun x => (f₂ x, f₃ x)) l (𝓤 α)
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ (fun x => (f₁ x, f₃ x)) ⁻¹' (s ○ s) ∈ l
[PROOFSTEP]
filter_upwards [mem_map.1 (h₁₂ hs), mem_map.1 (h₂₃ hs)] with x hx₁₂ hx₂₃ using ⟨_, hx₁₂, hx₂₃⟩
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
⊢ 𝓤 α ≤ Prod.swap <$> 𝓤 α
[PROOFSTEP]
rw [map_swap_eq_comap_swap]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
⊢ 𝓤 α ≤ comap Prod.swap (𝓤 α)
[PROOFSTEP]
exact tendsto_swap_uniformity.le_comap
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
V : Set (α × α)
h : V ∈ 𝓤 α
⊢ symmetrizeRel V ∈ 𝓤 α
[PROOFSTEP]
apply (𝓤 α).inter_sets h
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
V : Set (α × α)
h : V ∈ 𝓤 α
⊢ Prod.swap ⁻¹' V ∈ (𝓤 α).sets
[PROOFSTEP]
rw [← image_swap_eq_preimage_swap, uniformity_eq_symm]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
V : Set (α × α)
h : V ∈ 𝓤 α
⊢ Prod.swap '' V ∈ (Prod.swap <$> 𝓤 α).sets
[PROOFSTEP]
exact image_mem_map h
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
g : Set (α × α) → Filter β
f : Filter β
hg : Monotone g
h : (Filter.lift (𝓤 α) fun s => g (Prod.swap ⁻¹' s)) ≤ f
⊢ Filter.lift (map Prod.swap (𝓤 α)) g ≤ f
[PROOFSTEP]
rw [map_lift_eq2 hg, image_swap_eq_preimage_swap]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
g : Set (α × α) → Filter β
f : Filter β
hg : Monotone g
h : (Filter.lift (𝓤 α) fun s => g (Prod.swap ⁻¹' s)) ≤ f
⊢ Filter.lift (𝓤 α) (g ∘ preimage Prod.swap) ≤ f
[PROOFSTEP]
exact h
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
f : Set (α × α) → Filter β
h : Monotone f
⊢ (Filter.lift (𝓤 α) fun s => f (s ○ s)) = Filter.lift (Filter.lift' (𝓤 α) fun s => s ○ s) f
[PROOFSTEP]
rw [lift_lift'_assoc]
[GOAL]
case hg
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
f : Set (α × α) → Filter β
h : Monotone f
⊢ Monotone fun s => s ○ s
case hh
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
f : Set (α × α) → Filter β
h : Monotone f
⊢ Monotone f
[PROOFSTEP]
exact monotone_id.compRel monotone_id
[GOAL]
case hh
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
f : Set (α × α) → Filter β
h : Monotone f
⊢ Monotone f
[PROOFSTEP]
exact h
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∃ t, t ∈ 𝓤 α ∧ SymmetricRel t ∧ t ○ t ⊆ s
[PROOFSTEP]
obtain ⟨w, w_in, w_sub⟩ : ∃ w ∈ 𝓤 α, w ○ w ⊆ s := comp_mem_uniformity_sets hs
[GOAL]
case intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_sub : w ○ w ⊆ s
⊢ ∃ t, t ∈ 𝓤 α ∧ SymmetricRel t ∧ t ○ t ⊆ s
[PROOFSTEP]
use symmetrizeRel w, symmetrize_mem_uniformity w_in, symmetric_symmetrizeRel w
[GOAL]
case right
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_sub : w ○ w ⊆ s
⊢ symmetrizeRel w ○ symmetrizeRel w ⊆ s
[PROOFSTEP]
have : symmetrizeRel w ⊆ w := symmetrizeRel_subset_self w
[GOAL]
case right
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_sub : w ○ w ⊆ s
this : symmetrizeRel w ⊆ w
⊢ symmetrizeRel w ○ symmetrizeRel w ⊆ s
[PROOFSTEP]
calc
  symmetrizeRel w ○ symmetrizeRel w
  _ ⊆ w ○ w := by mono
  _ ⊆ s := w_sub
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_sub : w ○ w ⊆ s
this : symmetrizeRel w ⊆ w
⊢ symmetrizeRel w ○ symmetrizeRel w ⊆ w ○ w
[PROOFSTEP]
mono
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∃ t, t ∈ 𝓤 α ∧ SymmetricRel t ∧ t ○ t ○ t ⊆ s
[PROOFSTEP]
rcases comp_symm_mem_uniformity_sets hs with ⟨w, w_in, _, w_sub⟩
[GOAL]
case intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SymmetricRel w
w_sub : w ○ w ⊆ s
⊢ ∃ t, t ∈ 𝓤 α ∧ SymmetricRel t ∧ t ○ t ○ t ⊆ s
[PROOFSTEP]
rcases comp_symm_mem_uniformity_sets w_in with ⟨t, t_in, t_symm, t_sub⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SymmetricRel w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SymmetricRel t
t_sub : t ○ t ⊆ w
⊢ ∃ t, t ∈ 𝓤 α ∧ SymmetricRel t ∧ t ○ t ○ t ⊆ s
[PROOFSTEP]
use t, t_in, t_symm
[GOAL]
case right
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SymmetricRel w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SymmetricRel t
t_sub : t ○ t ⊆ w
⊢ t ○ t ○ t ⊆ s
[PROOFSTEP]
have : t ⊆ t ○ t := subset_comp_self_of_mem_uniformity t_in
[GOAL]
case right
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SymmetricRel w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SymmetricRel t
t_sub : t ○ t ⊆ w
this : t ⊆ t ○ t
⊢ t ○ t ○ t ⊆ s
[PROOFSTEP]
have ht := Subset.refl t
[GOAL]
case right
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SymmetricRel w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SymmetricRel t
t_sub : t ○ t ⊆ w
this : t ⊆ t ○ t
ht : t ⊆ t
⊢ t ○ t ○ t ⊆ s
[PROOFSTEP]
have hw := Subset.refl w
[GOAL]
case right
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SymmetricRel w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SymmetricRel t
t_sub : t ○ t ⊆ w
this : t ⊆ t ○ t
ht : t ⊆ t
hw : w ⊆ w
⊢ t ○ t ○ t ⊆ s
[PROOFSTEP]
calc
  t ○ t ○ t ⊆ w ○ t := by mono
  _ ⊆ w ○ (t ○ t) := by mono
  _ ⊆ w ○ w := by mono
  _ ⊆ s := w_sub
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SymmetricRel w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SymmetricRel t
t_sub : t ○ t ⊆ w
this : t ⊆ t ○ t
ht : t ⊆ t
hw : w ⊆ w
⊢ t ○ t ○ t ⊆ w ○ t
[PROOFSTEP]
mono
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SymmetricRel w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SymmetricRel t
t_sub : t ○ t ⊆ w
this : t ⊆ t ○ t
ht : t ⊆ t
hw : w ⊆ w
⊢ w ○ t ⊆ w ○ (t ○ t)
[PROOFSTEP]
mono
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SymmetricRel w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SymmetricRel t
t_sub : t ○ t ⊆ w
this : t ⊆ t ○ t
ht : t ⊆ t
hw : w ⊆ w
⊢ w ○ (t ○ t) ⊆ w ○ w
[PROOFSTEP]
mono
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
V : Set (β × β)
hV : SymmetricRel V
x y : β
⊢ (x, y) ∈ Prod.swap ⁻¹' V ↔ (x, y) ∈ V
[PROOFSTEP]
unfold SymmetricRel at hV 
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
V : Set (β × β)
hV : Prod.swap ⁻¹' V = V
x y : β
⊢ (x, y) ∈ Prod.swap ⁻¹' V ↔ (x, y) ∈ V
[PROOFSTEP]
rw [hV]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
V : Set (β × β)
hV : SymmetricRel V
x : β
⊢ ball x V = {y | (y, x) ∈ V}
[PROOFSTEP]
ext y
[GOAL]
case h
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
V : Set (β × β)
hV : SymmetricRel V
x y : β
⊢ y ∈ ball x V ↔ y ∈ {y | (y, x) ∈ V}
[PROOFSTEP]
rw [mem_ball_symmetry hV]
[GOAL]
case h
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
V : Set (β × β)
hV : SymmetricRel V
x y : β
⊢ x ∈ ball y V ↔ y ∈ {y | (y, x) ∈ V}
[PROOFSTEP]
exact Iff.rfl
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
V W : Set (β × β)
x y z : β
hV : SymmetricRel V
hx : x ∈ ball z V
hy : y ∈ ball z W
⊢ (x, y) ∈ V ○ W
[PROOFSTEP]
rw [mem_ball_symmetry hV] at hx 
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
V W : Set (β × β)
x y z : β
hV : SymmetricRel V
hx : z ∈ ball x V
hy : y ∈ ball z W
⊢ (x, y) ∈ V ○ W
[PROOFSTEP]
exact ⟨z, hx, hy⟩
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
V W M : Set (β × β)
hW' : SymmetricRel W
p : β × β
⊢ p ∈ V ○ M ○ W ↔ Set.Nonempty (ball p.fst V ×ˢ ball p.snd W ∩ M)
[PROOFSTEP]
cases' p with x y
[GOAL]
case mk
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
V W M : Set (β × β)
hW' : SymmetricRel W
x y : β
⊢ (x, y) ∈ V ○ M ○ W ↔ Set.Nonempty (ball (x, y).fst V ×ˢ ball (x, y).snd W ∩ M)
[PROOFSTEP]
constructor
[GOAL]
case mk.mp
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
V W M : Set (β × β)
hW' : SymmetricRel W
x y : β
⊢ (x, y) ∈ V ○ M ○ W → Set.Nonempty (ball (x, y).fst V ×ˢ ball (x, y).snd W ∩ M)
[PROOFSTEP]
rintro ⟨z, ⟨w, hpw, hwz⟩, hzy⟩
[GOAL]
case mk.mp.intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
V W M : Set (β × β)
hW' : SymmetricRel W
x y z : β
hzy : (z, (x, y).snd) ∈ W
w : β
hpw : (((x, y).fst, z).fst, w) ∈ V
hwz : (w, ((x, y).fst, z).snd) ∈ M
⊢ Set.Nonempty (ball (x, y).fst V ×ˢ ball (x, y).snd W ∩ M)
[PROOFSTEP]
exact ⟨(w, z), ⟨hpw, by rwa [mem_ball_symmetry hW']⟩, hwz⟩
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
V W M : Set (β × β)
hW' : SymmetricRel W
x y z : β
hzy : (z, (x, y).snd) ∈ W
w : β
hpw : (((x, y).fst, z).fst, w) ∈ V
hwz : (w, ((x, y).fst, z).snd) ∈ M
⊢ (w, z).snd ∈ ball (x, y).snd W
[PROOFSTEP]
rwa [mem_ball_symmetry hW']
[GOAL]
case mk.mpr
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
V W M : Set (β × β)
hW' : SymmetricRel W
x y : β
⊢ Set.Nonempty (ball (x, y).fst V ×ˢ ball (x, y).snd W ∩ M) → (x, y) ∈ V ○ M ○ W
[PROOFSTEP]
rintro ⟨⟨w, z⟩, ⟨w_in, z_in⟩, hwz⟩
[GOAL]
case mk.mpr.intro.mk.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
V W M : Set (β × β)
hW' : SymmetricRel W
x y w z : β
hwz : (w, z) ∈ M
w_in : (w, z).fst ∈ ball (x, y).fst V
z_in : (w, z).snd ∈ ball (x, y).snd W
⊢ (x, y) ∈ V ○ M ○ W
[PROOFSTEP]
rw [mem_ball_symmetry hW'] at z_in 
[GOAL]
case mk.mpr.intro.mk.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
V W M : Set (β × β)
hW' : SymmetricRel W
x y w z : β
hwz : (w, z) ∈ M
w_in : (w, z).fst ∈ ball (x, y).fst V
z_in : (x, y).snd ∈ ball (w, z).snd W
⊢ (x, y) ∈ V ○ M ○ W
[PROOFSTEP]
exact ⟨z, ⟨w, w_in, hwz⟩, z_in⟩
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
[PROOFSTEP]
refine' ⟨_, fun hs => _⟩
[GOAL]
case refine'_1
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
s : Set α
⊢ s ∈ 𝓝 x → {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
[PROOFSTEP]
simp only [mem_nhds_iff, isOpen_uniformity, and_imp, exists_imp]
[GOAL]
case refine'_1
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
s : Set α
⊢ ∀ (x_1 : Set α),
    x_1 ⊆ s → (∀ (x : α), x ∈ x_1 → {p | p.fst = x → p.snd ∈ x_1} ∈ 𝓤 α) → x ∈ x_1 → {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
[PROOFSTEP]
intro t ts ht xt
[GOAL]
case refine'_1
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
s t : Set α
ts : t ⊆ s
ht : ∀ (x : α), x ∈ t → {p | p.fst = x → p.snd ∈ t} ∈ 𝓤 α
xt : x ∈ t
⊢ {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
[PROOFSTEP]
filter_upwards [ht x xt] using fun y h eq => ts (h eq)
[GOAL]
case refine'_2
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
s : Set α
hs : {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
⊢ s ∈ 𝓝 x
[PROOFSTEP]
refine' mem_nhds_iff.mpr ⟨{x | {p : α × α | p.1 = x → p.2 ∈ s} ∈ 𝓤 α}, _, _, hs⟩
[GOAL]
case refine'_2.refine'_1
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
s : Set α
hs : {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
⊢ {x | {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α} ⊆ s
[PROOFSTEP]
exact fun y hy => refl_mem_uniformity hy rfl
[GOAL]
case refine'_2.refine'_2
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
s : Set α
hs : {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
⊢ IsOpen {x | {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α}
[PROOFSTEP]
refine' isOpen_uniformity.mpr fun y hy => _
[GOAL]
case refine'_2.refine'_2
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
s : Set α
hs : {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
y : α
hy : y ∈ {x | {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α}
⊢ {p | p.fst = y → p.snd ∈ {x | {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α}} ∈ 𝓤 α
[PROOFSTEP]
rcases comp_mem_uniformity_sets hy with ⟨t, ht, tr⟩
[GOAL]
case refine'_2.refine'_2.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
s : Set α
hs : {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
y : α
hy : y ∈ {x | {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α}
t : Set (α × α)
ht : t ∈ 𝓤 α
tr : t ○ t ⊆ {p | p.fst = y → p.snd ∈ s}
⊢ {p | p.fst = y → p.snd ∈ {x | {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α}} ∈ 𝓤 α
[PROOFSTEP]
filter_upwards [ht]
[GOAL]
case h
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
s : Set α
hs : {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
y : α
hy : y ∈ {x | {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α}
t : Set (α × α)
ht : t ∈ 𝓤 α
tr : t ○ t ⊆ {p | p.fst = y → p.snd ∈ s}
⊢ ∀ (a : α × α), a ∈ t → a.fst = y → {p | p.fst = a.snd → p.snd ∈ s} ∈ 𝓤 α
[PROOFSTEP]
rintro ⟨a, b⟩ hp' rfl
[GOAL]
case h.mk
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
s : Set α
hs : {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
t : Set (α × α)
ht : t ∈ 𝓤 α
a b : α
hp' : (a, b) ∈ t
hy : (a, b).fst ∈ {x | {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α}
tr : t ○ t ⊆ {p | p.fst = (a, b).fst → p.snd ∈ s}
⊢ {p | p.fst = (a, b).snd → p.snd ∈ s} ∈ 𝓤 α
[PROOFSTEP]
filter_upwards [ht]
[GOAL]
case h
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
s : Set α
hs : {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
t : Set (α × α)
ht : t ∈ 𝓤 α
a b : α
hp' : (a, b) ∈ t
hy : (a, b).fst ∈ {x | {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α}
tr : t ○ t ⊆ {p | p.fst = (a, b).fst → p.snd ∈ s}
⊢ ∀ (a : α × α), a ∈ t → a.fst = b → a.snd ∈ s
[PROOFSTEP]
rintro ⟨a', b'⟩ hp'' rfl
[GOAL]
case h.mk
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
s : Set α
hs : {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
t : Set (α × α)
ht : t ∈ 𝓤 α
a a' b' : α
hp'' : (a', b') ∈ t
hp' : (a, (a', b').fst) ∈ t
hy : (a, (a', b').fst).fst ∈ {x | {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α}
tr : t ○ t ⊆ {p | p.fst = (a, (a', b').fst).fst → p.snd ∈ s}
⊢ (a', b').snd ∈ s
[PROOFSTEP]
exact @tr (a, b') ⟨a', hp', hp''⟩ rfl
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ {p | p.snd = x → p.fst ∈ s} ∈ 𝓤 α
[PROOFSTEP]
rw [uniformity_eq_symm, mem_nhds_uniformity_iff_right]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
s : Set α
⊢ {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α ↔ {p | p.snd = x → p.fst ∈ s} ∈ Prod.swap <$> 𝓤 α
[PROOFSTEP]
simp only [map_def, mem_map, preimage_setOf_eq, Prod.snd_swap, Prod.fst_swap]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
⊢ 𝓝 x = comap (Prod.mk x) (𝓤 α)
[PROOFSTEP]
ext s
[GOAL]
case a
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ s ∈ comap (Prod.mk x) (𝓤 α)
[PROOFSTEP]
rw [mem_nhds_uniformity_iff_right, mem_comap_prod_mk]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set α
⊢ IsOpen s ↔ ∀ (x : α), x ∈ s → ∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s
[PROOFSTEP]
simp_rw [isOpen_iff_mem_nhds, nhds_eq_comap_uniformity, mem_comap, ball]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
h : HasBasis (𝓤 α) p s
x : α
⊢ HasBasis (𝓝 x) p fun i => ball x (s i)
[PROOFSTEP]
rw [nhds_eq_comap_uniformity]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
h : HasBasis (𝓤 α) p s
x : α
⊢ HasBasis (comap (Prod.mk x) (𝓤 α)) p fun i => ball x (s i)
[PROOFSTEP]
exact h.comap (Prod.mk x)
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
h : HasBasis (𝓤 α) p s
x : α
⊢ HasBasis (𝓝 x) p fun i => {y | (y, x) ∈ s i}
[PROOFSTEP]
replace h := h.comap Prod.swap
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
x : α
h : HasBasis (comap Prod.swap (𝓤 α)) p fun i => Prod.swap ⁻¹' s i
⊢ HasBasis (𝓝 x) p fun i => {y | (y, x) ∈ s i}
[PROOFSTEP]
rw [← map_swap_eq_comap_swap, ← uniformity_eq_symm] at h 
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
x : α
h : HasBasis (𝓤 α) p fun i => Prod.swap ⁻¹' s i
⊢ HasBasis (𝓝 x) p fun i => {y | (y, x) ∈ s i}
[PROOFSTEP]
exact nhds_basis_uniformity' h
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ ∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s
[PROOFSTEP]
rw [nhds_eq_comap_uniformity, mem_comap]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
s : Set α
⊢ (∃ t, t ∈ 𝓤 α ∧ Prod.mk x ⁻¹' t ⊆ s) ↔ ∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s
[PROOFSTEP]
simp_rw [ball]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
⊢ ball x V ∈ 𝓝 x
[PROOFSTEP]
rw [UniformSpace.mem_nhds_iff]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
⊢ ∃ V_1, V_1 ∈ 𝓤 α ∧ ball x V_1 ⊆ ball x V
[PROOFSTEP]
exact ⟨V, V_in, Subset.rfl⟩
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ ∃ V, V ∈ 𝓤 α ∧ SymmetricRel V ∧ ball x V ⊆ s
[PROOFSTEP]
rw [UniformSpace.mem_nhds_iff]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
s : Set α
⊢ (∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s) ↔ ∃ V, V ∈ 𝓤 α ∧ SymmetricRel V ∧ ball x V ⊆ s
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
s : Set α
⊢ (∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s) → ∃ V, V ∈ 𝓤 α ∧ SymmetricRel V ∧ ball x V ⊆ s
[PROOFSTEP]
rintro ⟨V, V_in, V_sub⟩
[GOAL]
case mp.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
s : Set α
V : Set (α × α)
V_in : V ∈ 𝓤 α
V_sub : ball x V ⊆ s
⊢ ∃ V, V ∈ 𝓤 α ∧ SymmetricRel V ∧ ball x V ⊆ s
[PROOFSTEP]
use symmetrizeRel V, symmetrize_mem_uniformity V_in, symmetric_symmetrizeRel V
[GOAL]
case right
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
s : Set α
V : Set (α × α)
V_in : V ∈ 𝓤 α
V_sub : ball x V ⊆ s
⊢ ball x (symmetrizeRel V) ⊆ s
[PROOFSTEP]
exact Subset.trans (ball_mono (symmetrizeRel_subset_self V) x) V_sub
[GOAL]
case mpr
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
s : Set α
⊢ (∃ V, V ∈ 𝓤 α ∧ SymmetricRel V ∧ ball x V ⊆ s) → ∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s
[PROOFSTEP]
rintro ⟨V, V_in, _, V_sub⟩
[GOAL]
case mpr.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
s : Set α
V : Set (α × α)
V_in : V ∈ 𝓤 α
left✝ : SymmetricRel V
V_sub : ball x V ⊆ s
⊢ ∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s
[PROOFSTEP]
exact ⟨V, V_in, V_sub⟩
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
t : Set α
⊢ t ∈ 𝓝 x ↔ ∃ i, (i ∈ 𝓤 α ∧ SymmetricRel i) ∧ ball x i ⊆ t
[PROOFSTEP]
simp [UniformSpace.mem_nhds_iff_symm, and_assoc]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set α
x : α
⊢ x ∈ closure s ↔ ∀ {V : Set (α × α)}, V ∈ 𝓤 α → SymmetricRel V → Set.Nonempty (s ∩ ball x V)
[PROOFSTEP]
simp [mem_closure_iff_nhds_basis (hasBasis_nhds x), Set.Nonempty]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set α
x : α
⊢ x ∈ closure s ↔ ∀ {V : Set (α × α)}, V ∈ 𝓤 α → Set.Nonempty (ball x V ∩ s)
[PROOFSTEP]
simp [mem_closure_iff_nhds_basis' (nhds_basis_uniformity' (𝓤 α).basis_sets)]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x y : α
⊢ HasBasis (𝓝 (x, y)) (fun s => s ∈ 𝓤 α ∧ SymmetricRel s) fun s => ball x s ×ˢ ball y s
[PROOFSTEP]
rw [nhds_prod_eq]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x y : α
⊢ HasBasis (𝓝 x ×ˢ 𝓝 y) (fun s => s ∈ 𝓤 α ∧ SymmetricRel s) fun s => ball x s ×ˢ ball y s
[PROOFSTEP]
apply (hasBasis_nhds x).prod_same_index (hasBasis_nhds y)
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x y : α
⊢ ∀ {i j : Set (α × α)},
    i ∈ 𝓤 α ∧ SymmetricRel i →
      j ∈ 𝓤 α ∧ SymmetricRel j → ∃ k, (k ∈ 𝓤 α ∧ SymmetricRel k) ∧ ball x k ⊆ ball x i ∧ ball y k ⊆ ball y j
[PROOFSTEP]
rintro U V ⟨U_in, U_symm⟩ ⟨V_in, V_symm⟩
[GOAL]
case intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x y : α
U V : Set (α × α)
U_in : U ∈ 𝓤 α
U_symm : SymmetricRel U
V_in : V ∈ 𝓤 α
V_symm : SymmetricRel V
⊢ ∃ k, (k ∈ 𝓤 α ∧ SymmetricRel k) ∧ ball x k ⊆ ball x U ∧ ball y k ⊆ ball y V
[PROOFSTEP]
exact ⟨U ∩ V, ⟨(𝓤 α).inter_sets U_in V_in, U_symm.inter V_symm⟩, ball_inter_left x U V, ball_inter_right y U V⟩
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
hU : HasBasis (𝓤 α) p s
K : Set α
hK : IsCompact K
⊢ HasBasis (𝓝ˢ K) p fun i => ⋃ (x : α) (_ : x ∈ K), ball x (s i)
[PROOFSTEP]
refine' ⟨fun U => _⟩
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
hU : HasBasis (𝓤 α) p s
K : Set α
hK : IsCompact K
U : Set α
⊢ U ∈ 𝓝ˢ K ↔ ∃ i, p i ∧ ⋃ (x : α) (_ : x ∈ K), ball x (s i) ⊆ U
[PROOFSTEP]
simp only [mem_nhdsSet_iff_forall, (nhds_basis_uniformity' hU).mem_iff, iUnion₂_subset_iff]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
hU : HasBasis (𝓤 α) p s
K : Set α
hK : IsCompact K
U : Set α
⊢ (∀ (x : α), x ∈ K → ∃ i, p i ∧ ball x (s i) ⊆ U) ↔ ∃ i, p i ∧ ∀ (i_1 : α), i_1 ∈ K → ball i_1 (s i) ⊆ U
[PROOFSTEP]
refine' ⟨fun H => _, fun ⟨i, hpi, hi⟩ x hx => ⟨i, hpi, hi x hx⟩⟩
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
hU : HasBasis (𝓤 α) p s
K : Set α
hK : IsCompact K
U : Set α
H : ∀ (x : α), x ∈ K → ∃ i, p i ∧ ball x (s i) ⊆ U
⊢ ∃ i, p i ∧ ∀ (i_1 : α), i_1 ∈ K → ball i_1 (s i) ⊆ U
[PROOFSTEP]
replace H : ∀ x ∈ K, ∃ i : { i // p i }, ball x (s i ○ s i) ⊆ U
[GOAL]
case H
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
hU : HasBasis (𝓤 α) p s
K : Set α
hK : IsCompact K
U : Set α
H : ∀ (x : α), x ∈ K → ∃ i, p i ∧ ball x (s i) ⊆ U
⊢ ∀ (x : α), x ∈ K → ∃ i, ball x (s ↑i ○ s ↑i) ⊆ U
[PROOFSTEP]
intro x hx
[GOAL]
case H
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
hU : HasBasis (𝓤 α) p s
K : Set α
hK : IsCompact K
U : Set α
H : ∀ (x : α), x ∈ K → ∃ i, p i ∧ ball x (s i) ⊆ U
x : α
hx : x ∈ K
⊢ ∃ i, ball x (s ↑i ○ s ↑i) ⊆ U
[PROOFSTEP]
rcases H x hx with ⟨i, hpi, hi⟩
[GOAL]
case H.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
hU : HasBasis (𝓤 α) p s
K : Set α
hK : IsCompact K
U : Set α
H : ∀ (x : α), x ∈ K → ∃ i, p i ∧ ball x (s i) ⊆ U
x : α
hx : x ∈ K
i : ι
hpi : p i
hi : ball x (s i) ⊆ U
⊢ ∃ i, ball x (s ↑i ○ s ↑i) ⊆ U
[PROOFSTEP]
rcases comp_mem_uniformity_sets (hU.mem_of_mem hpi) with ⟨t, ht_mem, ht⟩
[GOAL]
case H.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
K : Set α
hK : IsCompact K
U : Set α
H : ∀ (x : α), x ∈ K → ∃ i, p i ∧ ball x (s i) ⊆ U
x : α
hx : x ∈ K
i : ι
hpi : p i
hi : ball x (s i) ⊆ U
t : Set (α × α)
ht_mem : t ∈ 𝓤 α
ht : t ○ t ⊆ s i
⊢ ∃ i, ball x (s ↑i ○ s ↑i) ⊆ U
[PROOFSTEP]
rcases hU.mem_iff.1 ht_mem with ⟨j, hpj, hj⟩
[GOAL]
case H.intro.intro.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
K : Set α
hK : IsCompact K
U : Set α
H : ∀ (x : α), x ∈ K → ∃ i, p i ∧ ball x (s i) ⊆ U
x : α
hx : x ∈ K
i : ι
hpi : p i
hi : ball x (s i) ⊆ U
t : Set (α × α)
ht_mem : t ∈ 𝓤 α
ht : t ○ t ⊆ s i
j : ι
hpj : p j
hj : s j ⊆ t
⊢ ∃ i, ball x (s ↑i ○ s ↑i) ⊆ U
[PROOFSTEP]
exact ⟨⟨j, hpj⟩, Subset.trans (ball_mono ((compRel_mono hj hj).trans ht) _) hi⟩
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
hU : HasBasis (𝓤 α) p s
K : Set α
hK : IsCompact K
U : Set α
H : ∀ (x : α), x ∈ K → ∃ i, ball x (s ↑i ○ s ↑i) ⊆ U
⊢ ∃ i, p i ∧ ∀ (i_1 : α), i_1 ∈ K → ball i_1 (s i) ⊆ U
[PROOFSTEP]
have : Nonempty { a // p a } := nonempty_subtype.2 hU.ex_mem
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
hU : HasBasis (𝓤 α) p s
K : Set α
hK : IsCompact K
U : Set α
H : ∀ (x : α), x ∈ K → ∃ i, ball x (s ↑i ○ s ↑i) ⊆ U
this : Nonempty { a // p a }
⊢ ∃ i, p i ∧ ∀ (i_1 : α), i_1 ∈ K → ball i_1 (s i) ⊆ U
[PROOFSTEP]
choose! I hI using H
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
hU : HasBasis (𝓤 α) p s
K : Set α
hK : IsCompact K
U : Set α
this : Nonempty { a // p a }
I : α → { i // p i }
hI : ∀ (x : α), x ∈ K → ball x (s ↑(I x) ○ s ↑(I x)) ⊆ U
⊢ ∃ i, p i ∧ ∀ (i_1 : α), i_1 ∈ K → ball i_1 (s i) ⊆ U
[PROOFSTEP]
rcases hK.elim_nhds_subcover (fun x => ball x <| s (I x)) fun x _ => ball_mem_nhds _ <| hU.mem_of_mem (I x).2 with
  ⟨t, htK, ht⟩
[GOAL]
case intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
hU : HasBasis (𝓤 α) p s
K : Set α
hK : IsCompact K
U : Set α
this : Nonempty { a // p a }
I : α → { i // p i }
hI : ∀ (x : α), x ∈ K → ball x (s ↑(I x) ○ s ↑(I x)) ⊆ U
t : Finset α
htK : ∀ (x : α), x ∈ t → x ∈ K
ht : K ⊆ ⋃ (x : α) (_ : x ∈ t), ball x (s ↑(I x))
⊢ ∃ i, p i ∧ ∀ (i_1 : α), i_1 ∈ K → ball i_1 (s i) ⊆ U
[PROOFSTEP]
obtain ⟨i, hpi, hi⟩ : ∃ i, p i ∧ s i ⊆ ⋂ x ∈ t, s (I x)
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
hU : HasBasis (𝓤 α) p s
K : Set α
hK : IsCompact K
U : Set α
this : Nonempty { a // p a }
I : α → { i // p i }
hI : ∀ (x : α), x ∈ K → ball x (s ↑(I x) ○ s ↑(I x)) ⊆ U
t : Finset α
htK : ∀ (x : α), x ∈ t → x ∈ K
ht : K ⊆ ⋃ (x : α) (_ : x ∈ t), ball x (s ↑(I x))
⊢ ∃ i, p i ∧ s i ⊆ ⋂ (x : α) (_ : x ∈ t), s ↑(I x)
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
K : Set α
hK : IsCompact K
U : Set α
this : Nonempty { a // p a }
I : α → { i // p i }
hI : ∀ (x : α), x ∈ K → ball x (s ↑(I x) ○ s ↑(I x)) ⊆ U
t : Finset α
htK : ∀ (x : α), x ∈ t → x ∈ K
ht : K ⊆ ⋃ (x : α) (_ : x ∈ t), ball x (s ↑(I x))
i : ι
hpi : p i
hi : s i ⊆ ⋂ (x : α) (_ : x ∈ t), s ↑(I x)
⊢ ∃ i, p i ∧ ∀ (i_1 : α), i_1 ∈ K → ball i_1 (s i) ⊆ U
[PROOFSTEP]
exact hU.mem_iff.1 ((biInter_finset_mem t).2 fun x _ => hU.mem_of_mem (I x).2)
[GOAL]
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
K : Set α
hK : IsCompact K
U : Set α
this : Nonempty { a // p a }
I : α → { i // p i }
hI : ∀ (x : α), x ∈ K → ball x (s ↑(I x) ○ s ↑(I x)) ⊆ U
t : Finset α
htK : ∀ (x : α), x ∈ t → x ∈ K
ht : K ⊆ ⋃ (x : α) (_ : x ∈ t), ball x (s ↑(I x))
i : ι
hpi : p i
hi : s i ⊆ ⋂ (x : α) (_ : x ∈ t), s ↑(I x)
⊢ ∃ i, p i ∧ ∀ (i_1 : α), i_1 ∈ K → ball i_1 (s i) ⊆ U
[PROOFSTEP]
rw [subset_iInter₂_iff] at hi 
[GOAL]
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
K : Set α
hK : IsCompact K
U : Set α
this : Nonempty { a // p a }
I : α → { i // p i }
hI : ∀ (x : α), x ∈ K → ball x (s ↑(I x) ○ s ↑(I x)) ⊆ U
t : Finset α
htK : ∀ (x : α), x ∈ t → x ∈ K
ht : K ⊆ ⋃ (x : α) (_ : x ∈ t), ball x (s ↑(I x))
i : ι
hpi : p i
hi : ∀ (i_1 : α), i_1 ∈ t → s i ⊆ s ↑(I i_1)
⊢ ∃ i, p i ∧ ∀ (i_1 : α), i_1 ∈ K → ball i_1 (s i) ⊆ U
[PROOFSTEP]
refine' ⟨i, hpi, fun x hx => _⟩
[GOAL]
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
K : Set α
hK : IsCompact K
U : Set α
this : Nonempty { a // p a }
I : α → { i // p i }
hI : ∀ (x : α), x ∈ K → ball x (s ↑(I x) ○ s ↑(I x)) ⊆ U
t : Finset α
htK : ∀ (x : α), x ∈ t → x ∈ K
ht : K ⊆ ⋃ (x : α) (_ : x ∈ t), ball x (s ↑(I x))
i : ι
hpi : p i
hi : ∀ (i_1 : α), i_1 ∈ t → s i ⊆ s ↑(I i_1)
x : α
hx : x ∈ K
⊢ ball x (s i) ⊆ U
[PROOFSTEP]
rcases mem_iUnion₂.1 (ht hx) with ⟨z, hzt : z ∈ t, hzx : x ∈ ball z (s (I z))⟩
[GOAL]
case intro.intro.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
K : Set α
hK : IsCompact K
U : Set α
this : Nonempty { a // p a }
I : α → { i // p i }
hI : ∀ (x : α), x ∈ K → ball x (s ↑(I x) ○ s ↑(I x)) ⊆ U
t : Finset α
htK : ∀ (x : α), x ∈ t → x ∈ K
ht : K ⊆ ⋃ (x : α) (_ : x ∈ t), ball x (s ↑(I x))
i : ι
hpi : p i
hi : ∀ (i_1 : α), i_1 ∈ t → s i ⊆ s ↑(I i_1)
x : α
hx : x ∈ K
z : α
hzt : z ∈ t
hzx : x ∈ ball z (s ↑(I z))
⊢ ball x (s i) ⊆ U
[PROOFSTEP]
calc
  ball x (s i) ⊆ ball z (s (I z) ○ s (I z)) := fun y hy => ⟨x, hzx, hi z hzt hy⟩
  _ ⊆ U := hI z (htK z hzt)
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
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)
[PROOFSTEP]
have : Bᶜ ∈ 𝓝ˢ A := hB.isOpen_compl.mem_nhdsSet.mpr h.le_compl_right
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
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)
[PROOFSTEP]
rw [(hA.nhdsSet_basis_uniformity (Filter.basis_sets _)).mem_iff] at this 
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
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)
[PROOFSTEP]
rcases this with ⟨U, hU, hUAB⟩
[GOAL]
case intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
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)
[PROOFSTEP]
rcases comp_symm_mem_uniformity_sets hU with ⟨V, hV, hVsymm, hVU⟩
[GOAL]
case intro.intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
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)
[PROOFSTEP]
refine' ⟨V, hV, Set.disjoint_left.mpr fun x => _⟩
[GOAL]
case intro.intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
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
[PROOFSTEP]
simp only [mem_iUnion₂]
[GOAL]
case intro.intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
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
[PROOFSTEP]
rintro ⟨a, ha, hxa⟩ ⟨b, hb, hxb⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
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
[PROOFSTEP]
rw [mem_ball_symmetry hVsymm] at hxa hxb 
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
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
[PROOFSTEP]
exact hUAB (mem_iUnion₂_of_mem ha <| hVU <| mem_comp_of_mem_ball hVsymm hxa hxb) hb
[GOAL]
α : 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))
[PROOFSTEP]
rcases h.exists_uniform_thickening hA hB with ⟨V, hV, hVAB⟩
[GOAL]
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))
[PROOFSTEP]
rcases hU.mem_iff.1 hV with ⟨i, hi, hiV⟩
[GOAL]
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))
[PROOFSTEP]
exact ⟨i, hi, hVAB.mono (iUnion₂_mono fun a _ => ball_mono hiV a) (iUnion₂_mono fun b _ => ball_mono hiV b)⟩
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
g : Set α → Filter β
hg : Monotone g
⊢ Filter.lift (𝓝 x) g = Filter.lift (𝓤 α) fun s => g (ball x s)
[PROOFSTEP]
rw [nhds_eq_comap_uniformity, comap_lift_eq2 hg]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
g : Set α → Filter β
hg : Monotone g
⊢ Filter.lift (𝓤 α) (g ∘ preimage (Prod.mk x)) = Filter.lift (𝓤 α) fun s => g (ball x s)
[PROOFSTEP]
simp_rw [ball, Function.comp]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
g : Set α → Filter β
hg : Monotone g
⊢ Filter.lift (𝓝 x) g = Filter.lift (𝓤 α) fun s => g {y | (y, x) ∈ s}
[PROOFSTEP]
rw [nhds_eq_comap_uniformity', comap_lift_eq2 hg]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
g : Set α → Filter β
hg : Monotone g
⊢ Filter.lift (𝓤 α) (g ∘ preimage fun y => (y, x)) = Filter.lift (𝓤 α) fun s => g {y | (y, x) ∈ s}
[PROOFSTEP]
simp_rw [Function.comp, preimage]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
a b : α
⊢ 𝓝 a ×ˢ 𝓝 b = Filter.lift (𝓤 α) fun s => Filter.lift' (𝓤 α) fun t => {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}
[PROOFSTEP]
rw [nhds_eq_uniformity', nhds_eq_uniformity, prod_lift'_lift']
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
a b : α
⊢ (Filter.lift (𝓤 α) fun s => Filter.lift' (𝓤 α) fun t => {y | (y, a) ∈ s} ×ˢ ball b t) =
    Filter.lift (𝓤 α) fun s => Filter.lift' (𝓤 α) fun t => {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}
case hg₁
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
a b : α
⊢ Monotone fun s => {y | (y, a) ∈ s}
case hg₂ α : Type ua β : Type ub γ : Type uc δ : Type ud ι : Sort u_1 inst✝ : UniformSpace α a b : α ⊢ Monotone (ball b)
[PROOFSTEP]
exacts [rfl, monotone_preimage, monotone_preimage]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
a b : α
⊢ 𝓝 (a, b) = Filter.lift' (𝓤 α) fun s => {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ s}
[PROOFSTEP]
rw [nhds_prod_eq, nhds_nhds_eq_uniformity_uniformity_prod, lift_lift'_same_eq_lift']
[GOAL]
case hg₁
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
a b : α
⊢ ∀ (s : Set (α × α)), Monotone fun t => {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}
[PROOFSTEP]
exact fun s => monotone_const.set_prod monotone_preimage
[GOAL]
case hg₂
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
a b : α
⊢ ∀ (t : Set (α × α)), Monotone fun s => {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}
[PROOFSTEP]
refine fun t => Monotone.set_prod ?_ monotone_const
[GOAL]
case hg₂
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
a b : α
t : Set (α × α)
⊢ Monotone fun s => {y | (y, a) ∈ s}
[PROOFSTEP]
exact monotone_preimage (f := fun y => (y, a))
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
d s : Set (α × α)
hd : d ∈ 𝓤 α
⊢ ∃ t, IsOpen t ∧ s ⊆ t ∧ t ⊆ {p | ∃ x y, (p.fst, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.snd) ∈ d}
[PROOFSTEP]
let cl_d := {p : α × α | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
d s : Set (α × α)
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.fst, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.snd) ∈ d}
⊢ ∃ t, IsOpen t ∧ s ⊆ t ∧ t ⊆ {p | ∃ x y, (p.fst, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.snd) ∈ d}
[PROOFSTEP]
have : ∀ p ∈ s, ∃ t, t ⊆ cl_d ∧ IsOpen t ∧ p ∈ t := fun ⟨x, y⟩ hp =>
  mem_nhds_iff.mp <|
    show cl_d ∈ 𝓝 (x, y) by
      rw [nhds_eq_uniformity_prod, mem_lift'_sets]
      · exact ⟨d, hd, fun ⟨a, b⟩ ⟨ha, hb⟩ => ⟨x, y, ha, hp, hb⟩⟩
      · exact fun _ _ h _ h' => ⟨h h'.1, h h'.2⟩
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
d s : Set (α × α)
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.fst, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.snd) ∈ d}
x✝ : α × α
x y : α
hp : (x, y) ∈ s
⊢ cl_d ∈ 𝓝 (x, y)
[PROOFSTEP]
rw [nhds_eq_uniformity_prod, mem_lift'_sets]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
d s : Set (α × α)
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.fst, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.snd) ∈ d}
x✝ : α × α
x y : α
hp : (x, y) ∈ s
⊢ ∃ t, t ∈ 𝓤 α ∧ {y | (y, x) ∈ t} ×ˢ {y_1 | (y, y_1) ∈ t} ⊆ cl_d
[PROOFSTEP]
exact ⟨d, hd, fun ⟨a, b⟩ ⟨ha, hb⟩ => ⟨x, y, ha, hp, hb⟩⟩
[GOAL]
case hh
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
d s : Set (α × α)
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.fst, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.snd) ∈ d}
x✝ : α × α
x y : α
hp : (x, y) ∈ s
⊢ Monotone fun s => {y | (y, x) ∈ s} ×ˢ {y_1 | (y, y_1) ∈ s}
[PROOFSTEP]
exact fun _ _ h _ h' => ⟨h h'.1, h h'.2⟩
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
d s : Set (α × α)
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.fst, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.snd) ∈ d}
this : ∀ (p : α × α), p ∈ s → ∃ t, t ⊆ cl_d ∧ IsOpen t ∧ p ∈ t
⊢ ∃ t, IsOpen t ∧ s ⊆ t ∧ t ⊆ {p | ∃ x y, (p.fst, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.snd) ∈ d}
[PROOFSTEP]
choose t ht using this
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
d s : Set (α × α)
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.fst, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.snd) ∈ d}
t : (p : α × α) → p ∈ s → Set (α × α)
ht : ∀ (p : α × α) (a : p ∈ s), t p a ⊆ cl_d ∧ IsOpen (t p a) ∧ p ∈ t p a
⊢ ∃ t, IsOpen t ∧ s ⊆ t ∧ t ⊆ {p | ∃ x y, (p.fst, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.snd) ∈ d}
[PROOFSTEP]
exact
  ⟨(⋃ p : α × α, ⋃ h : p ∈ s, t p h : Set (α × α)),
    isOpen_iUnion fun p : α × α => isOpen_iUnion fun hp => (ht p hp).right.left, fun ⟨a, b⟩ hp => by
    simp only [mem_iUnion, Prod.exists]; exact ⟨a, b, hp, (ht (a, b) hp).right.right⟩,
    iUnion_subset fun p => iUnion_subset fun hp => (ht p hp).left⟩
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
d s : Set (α × α)
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.fst, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.snd) ∈ d}
t : (p : α × α) → p ∈ s → Set (α × α)
ht : ∀ (p : α × α) (a : p ∈ s), t p a ⊆ cl_d ∧ IsOpen (t p a) ∧ p ∈ t p a
x✝ : α × α
a b : α
hp : (a, b) ∈ s
⊢ (a, b) ∈ ⋃ (p : α × α) (h : p ∈ s), t p h
[PROOFSTEP]
simp only [mem_iUnion, Prod.exists]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
d s : Set (α × α)
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.fst, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.snd) ∈ d}
t : (p : α × α) → p ∈ s → Set (α × α)
ht : ∀ (p : α × α) (a : p ∈ s), t p a ⊆ cl_d ∧ IsOpen (t p a) ∧ p ∈ t p a
x✝ : α × α
a b : α
hp : (a, b) ∈ s
⊢ ∃ a_1 b_1 i, (a, b) ∈ t (a_1, b_1) i
[PROOFSTEP]
exact ⟨a, b, hp, (ht (a, b) hp).right.right⟩
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
⊢ 𝓝 (x, x) ≤ 𝓤 α
[PROOFSTEP]
intro V V_in
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
⊢ V ∈ 𝓝 (x, x)
[PROOFSTEP]
rcases comp_symm_mem_uniformity_sets V_in with ⟨w, w_in, w_symm, w_sub⟩
[GOAL]
case intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
w_sub : w ○ w ⊆ V
⊢ V ∈ 𝓝 (x, x)
[PROOFSTEP]
have : ball x w ×ˢ ball x w ∈ 𝓝 (x, x)
[GOAL]
case this
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
w_sub : w ○ w ⊆ V
⊢ ball x w ×ˢ ball x w ∈ 𝓝 (x, x)
[PROOFSTEP]
rw [nhds_prod_eq]
[GOAL]
case this
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
w_sub : w ○ w ⊆ V
⊢ ball x w ×ˢ ball x w ∈ 𝓝 x ×ˢ 𝓝 x
[PROOFSTEP]
exact prod_mem_prod (ball_mem_nhds x w_in) (ball_mem_nhds x w_in)
[GOAL]
case intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
w_sub : w ○ w ⊆ V
this : ball x w ×ˢ ball x w ∈ 𝓝 (x, x)
⊢ V ∈ 𝓝 (x, x)
[PROOFSTEP]
apply mem_of_superset this
[GOAL]
case intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
w_sub : w ○ w ⊆ V
this : ball x w ×ˢ ball x w ∈ 𝓝 (x, x)
⊢ ball x w ×ˢ ball x w ⊆ V
[PROOFSTEP]
rintro ⟨u, v⟩ ⟨u_in, v_in⟩
[GOAL]
case intro.intro.intro.mk.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
w_sub : w ○ w ⊆ V
this : ball x w ×ˢ ball x w ∈ 𝓝 (x, x)
u v : α
u_in : (u, v).fst ∈ ball x w
v_in : (u, v).snd ∈ ball x w
⊢ (u, v) ∈ V
[PROOFSTEP]
exact w_sub (mem_comp_of_mem_ball w_symm u_in v_in)
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set (α × α)
⊢ closure s = ⋂ (V : Set (α × α)) (_ : V ∈ {V | V ∈ 𝓤 α ∧ SymmetricRel V}), V ○ s ○ V
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case h.mk
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set (α × α)
x y : α
⊢ (x, y) ∈ closure s ↔ (x, y) ∈ ⋂ (V : Set (α × α)) (_ : V ∈ {V | V ∈ 𝓤 α ∧ SymmetricRel V}), V ○ s ○ V
[PROOFSTEP]
simp (config := { contextual := true }) only [mem_closure_iff_nhds_basis (UniformSpace.hasBasis_nhds_prod x y),
  mem_iInter, mem_setOf_eq, and_imp, mem_comp_comp, exists_prop, ← mem_inter_iff, inter_comm, Set.Nonempty]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
⊢ HasBasis (𝓤 α) (fun V => V ∈ 𝓤 α ∧ IsClosed V) id
[PROOFSTEP]
refine' Filter.hasBasis_self.2 fun t h => _
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
⊢ ∃ r, r ∈ 𝓤 α ∧ IsClosed r ∧ r ⊆ t
[PROOFSTEP]
rcases comp_comp_symm_mem_uniformity_sets h with ⟨w, w_in, w_symm, r⟩
[GOAL]
case intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
r : w ○ w ○ w ⊆ t
⊢ ∃ r, r ∈ 𝓤 α ∧ IsClosed r ∧ r ⊆ t
[PROOFSTEP]
refine' ⟨closure w, mem_of_superset w_in subset_closure, isClosed_closure, _⟩
[GOAL]
case intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
r : w ○ w ○ w ⊆ t
⊢ closure w ⊆ t
[PROOFSTEP]
refine' Subset.trans _ r
[GOAL]
case intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
r : w ○ w ○ w ⊆ t
⊢ closure w ⊆ w ○ w ○ w
[PROOFSTEP]
rw [closure_eq_uniformity]
[GOAL]
case intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
r : w ○ w ○ w ⊆ t
⊢ ⋂ (V : Set (α × α)) (_ : V ∈ {V | V ∈ 𝓤 α ∧ SymmetricRel V}), V ○ w ○ V ⊆ w ○ w ○ w
[PROOFSTEP]
apply iInter_subset_of_subset
[GOAL]
case intro.intro.intro.h
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
r : w ○ w ○ w ⊆ t
⊢ ⋂ (_ : ?intro.intro.intro.i ∈ {V | V ∈ 𝓤 α ∧ SymmetricRel V}), ?intro.intro.intro.i ○ w ○ ?intro.intro.intro.i ⊆
    w ○ w ○ w
case intro.intro.intro.i
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
r : w ○ w ○ w ⊆ t
⊢ Set (α × α)
[PROOFSTEP]
apply iInter_subset
[GOAL]
case intro.intro.intro.h.i
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
r : w ○ w ○ w ⊆ t
⊢ w ∈ {V | V ∈ 𝓤 α ∧ SymmetricRel V}
[PROOFSTEP]
exact ⟨w_in, w_symm⟩
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
t : Set (α × α)
⊢ ⋂ (V : Set (α × α)) (_ : V ∈ 𝓤 α), V ○ t ○ V = ⋂ (V : Set (α × α)) (_ : V ∈ 𝓤 α), V ○ (t ○ V)
[PROOFSTEP]
simp only [compRel_assoc]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d
[PROOFSTEP]
let ⟨s, hs, hs_comp⟩ := comp3_mem_uniformity hd
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d
[PROOFSTEP]
let ⟨t, ht, hst, ht_comp⟩ := nhdset_of_mem_uniformity s hs
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
t : Set (α × α)
ht : IsOpen t
hst : s ⊆ t
ht_comp : t ⊆ {p | ∃ x y, (p.fst, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.snd) ∈ s}
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d
[PROOFSTEP]
have : s ⊆ interior d :=
  calc
    s ⊆ t := hst
    _ ⊆ interior d :=
      ht.subset_interior_iff.mpr fun x (hx : x ∈ t) =>
        let ⟨x, y, h₁, h₂, h₃⟩ := ht_comp hx
        hs_comp ⟨x, h₁, y, h₂, h₃⟩
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
t : Set (α × α)
ht : IsOpen t
hst : s ⊆ t
ht_comp : t ⊆ {p | ∃ x y, (p.fst, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.snd) ∈ s}
this : s ⊆ interior d
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d
[PROOFSTEP]
have : interior d ∈ 𝓤 α := by filter_upwards [hs] using this
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
t : Set (α × α)
ht : IsOpen t
hst : s ⊆ t
ht_comp : t ⊆ {p | ∃ x y, (p.fst, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.snd) ∈ s}
this : s ⊆ interior d
⊢ interior d ∈ 𝓤 α
[PROOFSTEP]
filter_upwards [hs] using this
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
t : Set (α × α)
ht : IsOpen t
hst : s ⊆ t
ht_comp : t ⊆ {p | ∃ x y, (p.fst, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.snd) ∈ s}
this✝ : s ⊆ interior d
this : interior d ∈ 𝓤 α
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d
[PROOFSTEP]
simp [this]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ interior s ∈ 𝓤 α
[PROOFSTEP]
rw [uniformity_eq_uniformity_interior]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ interior s ∈ Filter.lift' (𝓤 α) interior
[PROOFSTEP]
exact mem_lift' hs
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set α
⊢ IsOpen s ↔ ∀ (x : α), x ∈ s → ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ ball x V ⊆ s
[PROOFSTEP]
rw [isOpen_iff_ball_subset]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set α
⊢ (∀ (x : α), x ∈ s → ∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s) ↔ ∀ (x : α), x ∈ s → ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ ball x V ⊆ s
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set α
⊢ (∀ (x : α), x ∈ s → ∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s) → ∀ (x : α), x ∈ s → ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ ball x V ⊆ s
[PROOFSTEP]
intro h x hx
[GOAL]
case mpr
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set α
⊢ (∀ (x : α), x ∈ s → ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ ball x V ⊆ s) → ∀ (x : α), x ∈ s → ∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s
[PROOFSTEP]
intro h x hx
[GOAL]
case mp
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set α
h : ∀ (x : α), x ∈ s → ∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s
x : α
hx : x ∈ s
⊢ ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ ball x V ⊆ s
[PROOFSTEP]
obtain ⟨V, hV, hV'⟩ := h x hx
[GOAL]
case mp.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set α
h : ∀ (x : α), x ∈ s → ∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s
x : α
hx : x ∈ s
V : Set (α × α)
hV : V ∈ 𝓤 α
hV' : ball x V ⊆ s
⊢ ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ ball x V ⊆ s
[PROOFSTEP]
exact ⟨interior V, interior_mem_uniformity hV, isOpen_interior, (ball_mono interior_subset x).trans hV'⟩
[GOAL]
case mpr
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set α
h : ∀ (x : α), x ∈ s → ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ ball x V ⊆ s
x : α
hx : x ∈ s
⊢ ∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s
[PROOFSTEP]
obtain ⟨V, hV, -, hV'⟩ := h x hx
[GOAL]
case mpr.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set α
h : ∀ (x : α), x ∈ s → ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ ball x V ⊆ s
x : α
hx : x ∈ s
V : Set (α × α)
hV : V ∈ 𝓤 α
hV' : ball x V ⊆ s
⊢ ∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s
[PROOFSTEP]
exact ⟨V, hV, hV'⟩
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set α
U : Set (α × α)
hs : Dense s
hU : U ∈ 𝓤 α
⊢ ⋃ (x : α) (_ : x ∈ s), ball x U = univ
[PROOFSTEP]
refine' iUnion₂_eq_univ_iff.2 fun y => _
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set α
U : Set (α × α)
hs : Dense s
hU : U ∈ 𝓤 α
y : α
⊢ ∃ i j, y ∈ ball i U
[PROOFSTEP]
rcases hs.inter_nhds_nonempty (mem_nhds_right y hU) with ⟨x, hxs, hxy : (x, y) ∈ U⟩
[GOAL]
case intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set α
U : Set (α × α)
hs : Dense s
hU : U ∈ 𝓤 α
y x : α
hxs : x ∈ s
hxy : (x, y) ∈ U
⊢ ∃ i j, y ∈ ball i U
[PROOFSTEP]
exact ⟨x, hxs, hxy⟩
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : β → Prop
s : β → Set (α × α)
h : HasBasis (𝓤 α) p s
t : Set (α × α)
⊢ (∃ i, p i ∧ s i ⊆ t) ↔ ∃ i, p i ∧ ∀ (a b : α), (a, b) ∈ s i → (a, b) ∈ t
[PROOFSTEP]
simp only [Prod.forall, subset_def]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
⊢ HasBasis (𝓤 α) (fun V => V ∈ 𝓤 α ∧ IsOpen V ∧ SymmetricRel V) id
[PROOFSTEP]
simp only [← and_assoc]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
⊢ HasBasis (𝓤 α) (fun V => (V ∈ 𝓤 α ∧ IsOpen V) ∧ SymmetricRel V) id
[PROOFSTEP]
refine' uniformity_hasBasis_open.restrict fun s hs => ⟨symmetrizeRel s, _⟩
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α ∧ IsOpen s
⊢ (symmetrizeRel s ∈ 𝓤 α ∧ IsOpen (symmetrizeRel s)) ∧ SymmetricRel (symmetrizeRel s) ∧ id (symmetrizeRel s) ⊆ id s
[PROOFSTEP]
exact
  ⟨⟨symmetrize_mem_uniformity hs.1, IsOpen.inter hs.2 (hs.2.preimage continuous_swap)⟩, symmetric_symmetrizeRel s,
    symmetrizeRel_subset_self s⟩
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∃ t, t ∈ 𝓤 α ∧ IsOpen t ∧ SymmetricRel t ∧ t ○ t ⊆ s
[PROOFSTEP]
obtain ⟨t, ht₁, ht₂⟩ := comp_mem_uniformity_sets hs
[GOAL]
case intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
ht₁ : t ∈ 𝓤 α
ht₂ : t ○ t ⊆ s
⊢ ∃ t, t ∈ 𝓤 α ∧ IsOpen t ∧ SymmetricRel t ∧ t ○ t ⊆ s
[PROOFSTEP]
obtain ⟨u, ⟨hu₁, hu₂, hu₃⟩, hu₄ : u ⊆ t⟩ := uniformity_hasBasis_open_symmetric.mem_iff.mp ht₁
[GOAL]
case intro.intro.intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
ht₁ : t ∈ 𝓤 α
ht₂ : t ○ t ⊆ s
u : Set (α × α)
hu₄ : u ⊆ t
hu₁ : u ∈ 𝓤 α
hu₂ : IsOpen u
hu₃ : SymmetricRel u
⊢ ∃ t, t ∈ 𝓤 α ∧ IsOpen t ∧ SymmetricRel t ∧ t ○ t ⊆ s
[PROOFSTEP]
exact ⟨u, hu₁, hu₂, hu₃, (compRel_mono hu₄ hu₄).trans ht₂⟩
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
U : ι → Set (α × α)
h : HasBasis (𝓤 α) p U
s : Set α
⊢ ⋂ (i : ι) (_ : p i), ⋃ (x : α) (_ : x ∈ s), ball x (U i) = closure s
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
U : ι → Set (α × α)
h : HasBasis (𝓤 α) p U
s : Set α
x : α
⊢ x ∈ ⋂ (i : ι) (_ : p i), ⋃ (x : α) (_ : x ∈ s), ball x (U i) ↔ x ∈ closure s
[PROOFSTEP]
simp [mem_closure_iff_nhds_basis (nhds_basis_uniformity h), ball]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
⊢ UniformContinuousOn f univ ↔ UniformContinuous f
[PROOFSTEP]
rw [UniformContinuousOn, UniformContinuous, univ_prod_univ, principal_univ, inf_top_eq]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
c : α → β
h : ∀ (a b : α), c a = c b
this : (fun x => (c x.fst, c x.snd)) ⁻¹' idRel = univ
⊢ 𝓤 α ≤ comap (fun x => (c x.fst, c x.snd)) (𝓟 idRel)
[PROOFSTEP]
simp [comap_principal, this, univ_mem]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
ι' : Sort u_2
inst✝ : UniformSpace β
p : ι → Prop
s : ι → Set (α × α)
ha : HasBasis (𝓤 α) p s
q : ι' → Prop
t : ι' → Set (β × β)
hb : HasBasis (𝓤 β) q t
f : α → β
⊢ (∀ (ib : ι'), q ib → ∃ ia, p ia ∧ ∀ (x : α × α), x ∈ s ia → (f x.fst, f x.snd) ∈ t ib) ↔
    ∀ (i : ι'), q i → ∃ j, p j ∧ ∀ (x y : α), (x, y) ∈ s j → (f x, f y) ∈ t i
[PROOFSTEP]
simp only [Prod.forall]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
ι' : Sort u_2
inst✝ : UniformSpace β
p : ι → Prop
s : ι → Set (α × α)
ha : HasBasis (𝓤 α) p s
q : ι' → Prop
t : ι' → Set (β × β)
hb : HasBasis (𝓤 β) q t
f : α → β
S : Set α
⊢ (∀ (ib : ι'), q ib → ∃ ia, p ia ∧ ∀ (x : α × α), x ∈ s ia ∩ S ×ˢ S → (f x.fst, f x.snd) ∈ t ib) ↔
    ∀ (i : ι'), q i → ∃ j, p j ∧ ∀ (x : α), x ∈ S → ∀ (y : α), y ∈ S → (x, y) ∈ s j → (f x, f y) ∈ t i
[PROOFSTEP]
simp_rw [Prod.forall, Set.inter_comm (s _), ball_mem_comm, mem_inter_iff, mem_prod, and_imp]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
⊢ Tendsto Prod.swap (𝓟 idRel) (𝓟 idRel)
[PROOFSTEP]
simp [Tendsto]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
s : Set α
⊢ IsOpen s ↔
    ∀ (x : α),
      x ∈ s →
        {p | p.fst = x → p.snd ∈ s} ∈
          { uniformity := 𝓟 idRel, refl := (_ : 𝓟 idRel ≤ 𝓟 idRel), symm := (_ : map Prod.swap (𝓟 idRel) ≤ 𝓟 idRel),
              comp := (_ : (Filter.lift' (𝓟 idRel) fun s => s ○ s) ≤ 𝓟 idRel) }.uniformity
[PROOFSTEP]
let _ : TopologicalSpace α := ⊥
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
s : Set α
x✝ : TopologicalSpace α := ⊥
⊢ IsOpen s ↔
    ∀ (x : α),
      x ∈ s →
        {p | p.fst = x → p.snd ∈ s} ∈
          { uniformity := 𝓟 idRel, refl := (_ : 𝓟 idRel ≤ 𝓟 idRel), symm := (_ : map Prod.swap (𝓟 idRel) ≤ 𝓟 idRel),
              comp := (_ : (Filter.lift' (𝓟 idRel) fun s => s ○ s) ≤ 𝓟 idRel) }.uniformity
[PROOFSTEP]
have := discreteTopology_bot α
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
s : Set α
x✝ : TopologicalSpace α := ⊥
this : DiscreteTopology α
⊢ IsOpen s ↔
    ∀ (x : α),
      x ∈ s →
        {p | p.fst = x → p.snd ∈ s} ∈
          { uniformity := 𝓟 idRel, refl := (_ : 𝓟 idRel ≤ 𝓟 idRel), symm := (_ : map Prod.swap (𝓟 idRel) ≤ 𝓟 idRel),
              comp := (_ : (Filter.lift' (𝓟 idRel) fun s => s ○ s) ≤ 𝓟 idRel) }.uniformity
[PROOFSTEP]
simp [subset_def, idRel]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
u₁ u₂ : UniformSpace α
x✝ : α
⊢ 𝓝 x✝ =
    comap (Prod.mk x✝)
      { uniformity := u₁.uniformity ⊓ u₂.uniformity, refl := (_ : 𝓟 idRel ≤ u₁.uniformity ⊓ u₂.uniformity),
          symm := (_ : Tendsto Prod.swap (u₁.uniformity ⊓ u₂.uniformity) (u₁.uniformity ⊓ u₂.uniformity)),
          comp :=
            (_ :
              (Filter.lift' (u₁.uniformity ⊓ u₂.uniformity) fun s => s ○ s) ≤
                u₁.uniformity ⊓ u₂.uniformity) }.uniformity
[PROOFSTEP]
rw [@nhds_inf _ u₁.toTopologicalSpace u₂.toTopologicalSpace, @nhds_eq_comap_uniformity _ u₁,
  @nhds_eq_comap_uniformity _ u₂, comap_inf]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
u₁ u₂ : UniformSpace α
x✝ : α
⊢ comap (Prod.mk x✝) (𝓤 α) ⊓ comap (Prod.mk x✝) (𝓤 α) =
    comap (Prod.mk x✝) u₁.uniformity ⊓ comap (Prod.mk x✝) u₂.uniformity
[PROOFSTEP]
rfl
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u : UniformSpace β
⊢ 𝓟 idRel ≤ Filter.comap (fun p => (f p.fst, f p.snd)) (𝓟 idRel)
[PROOFSTEP]
simp
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u : UniformSpace β
⊢ Tendsto Prod.swap (Filter.comap (fun p => (f p.fst, f p.snd)) (𝓤 β))
    (Filter.comap (fun p => (f p.fst, f p.snd)) (𝓤 β))
[PROOFSTEP]
simp only [tendsto_comap_iff, Prod.swap, (· ∘ ·)]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u : UniformSpace β
⊢ Tendsto (fun x => (f x.snd, f x.fst)) (Filter.comap (fun p => (f p.fst, f p.snd)) (𝓤 β)) (𝓤 β)
[PROOFSTEP]
exact tendsto_swap_uniformity.comp tendsto_comap
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u : UniformSpace β
⊢ (Filter.lift' (Filter.comap (fun p => (f p.fst, f p.snd)) (𝓤 β)) fun s => s ○ s) ≤
    Filter.comap (fun p => (f p.fst, f p.snd)) (Filter.lift' u.uniformity fun s => s ○ s)
[PROOFSTEP]
rw [comap_lift'_eq, comap_lift'_eq2]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u : UniformSpace β
⊢ Filter.lift' (𝓤 β) ((fun s => s ○ s) ∘ preimage fun p => (f p.fst, f p.snd)) ≤
    Filter.lift' u.uniformity ((preimage fun p => (f p.fst, f p.snd)) ∘ fun s => s ○ s)
α : Type ua β : Type ub γ : Type uc δ : Type ud ι : Sort u_1 f : α → β u : UniformSpace β ⊢ Monotone fun s => s ○ s
[PROOFSTEP]
exact lift'_mono' fun s _ ⟨a₁, a₂⟩ ⟨x, h₁, h₂⟩ => ⟨f x, h₁, h₂⟩
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u : UniformSpace β
⊢ Monotone fun s => s ○ s
[PROOFSTEP]
exact monotone_id.compRel monotone_id
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u : UniformSpace β
x : α
⊢ 𝓝 x =
    Filter.comap (Prod.mk x)
      { uniformity := Filter.comap (fun p => (f p.fst, f p.snd)) (𝓤 β),
          refl := (_ : 𝓟 idRel ≤ Filter.comap (fun p => (f p.fst, f p.snd)) (𝓤 β)),
          symm :=
            (_ :
              Tendsto Prod.swap (Filter.comap (fun p => (f p.fst, f p.snd)) (𝓤 β))
                (Filter.comap (fun p => (f p.fst, f p.snd)) (𝓤 β))),
          comp :=
            (_ :
              (Filter.lift' (Filter.comap (fun p => (f p.fst, f p.snd)) (𝓤 β)) fun s => s ○ s) ≤
                Filter.comap (fun p => (f p.fst, f p.snd)) (𝓤 β)) }.uniformity
[PROOFSTEP]
simp only [nhds_induced, nhds_eq_comap_uniformity, comap_comap, Function.comp]
[GOAL]
α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
α : Type u_2
⊢ UniformSpace.comap id = id
[PROOFSTEP]
ext : 2
[GOAL]
case h.a
α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
α : Type u_2
x✝ : UniformSpace α
⊢ 𝓤 α = 𝓤 α
[PROOFSTEP]
rw [uniformity_comap, Prod.map_id, comap_id]
[GOAL]
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
uγ : UniformSpace γ
f : α → β
g : β → γ
⊢ comap (g ∘ f) uγ = comap f (comap g uγ)
[PROOFSTEP]
ext1
[GOAL]
case a
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
uγ : UniformSpace γ
f : α → β
g : β → γ
⊢ 𝓤 α = 𝓤 α
[PROOFSTEP]
simp only [uniformity_comap, Filter.comap_comap, Prod.map_comp_map]
[GOAL]
α✝ : Type ua
β : Type ub
γ✝ : Type uc
δ : Type ud
ι✝ : Sort u_1
ι : Sort u_2
α : Type u_3
γ : Type u_4
u : ι → UniformSpace γ
f : α → γ
⊢ comap f (⨅ (i : ι), u i) = ⨅ (i : ι), comap f (u i)
[PROOFSTEP]
ext : 1
[GOAL]
case a
α✝ : Type ua
β : Type ub
γ✝ : Type uc
δ : Type ud
ι✝ : Sort u_1
ι : Sort u_2
α : Type u_3
γ : Type u_4
u : ι → UniformSpace γ
f : α → γ
⊢ 𝓤 α = 𝓤 α
[PROOFSTEP]
simp [uniformity_comap, iInf_uniformity]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
u v : UniformSpace α
⊢ u ≤ v ↔ UniformContinuous id
[PROOFSTEP]
rw [uniformContinuous_iff, uniformSpace_comap_id, id]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
u₁ u₂ : UniformSpace α
h : u₁ ≤ u₂
a : α
⊢ 𝓝 a ≤ 𝓝 a
[PROOFSTEP]
rw [@nhds_eq_uniformity α u₁ a, @nhds_eq_uniformity α u₂ a]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
u₁ u₂ : UniformSpace α
h : u₁ ≤ u₂
a : α
⊢ Filter.lift' (𝓤 α) (UniformSpace.ball a) ≤ Filter.lift' (𝓤 α) (UniformSpace.ball a)
[PROOFSTEP]
exact lift'_mono h le_rfl
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι✝ : Sort u_1
ι : Sort u_2
u : ι → UniformSpace α
a : α
⊢ 𝓝 a = 𝓝 a
[PROOFSTEP]
simp only [@nhds_eq_comap_uniformity _ (iInf u), nhds_iInf, iInf_uniformity, @nhds_eq_comap_uniformity _ (u _),
  comap_iInf]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
s : Set (UniformSpace α)
⊢ UniformSpace.toTopologicalSpace = ⨅ (i : UniformSpace α) (_ : i ∈ s), UniformSpace.toTopologicalSpace
[PROOFSTEP]
rw [sInf_eq_iInf]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
s : Set (UniformSpace α)
⊢ UniformSpace.toTopologicalSpace = ⨅ (i : UniformSpace α) (_ : i ∈ s), UniformSpace.toTopologicalSpace
[PROOFSTEP]
simp only [← toTopologicalSpace_iInf]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u₁ : Set (UniformSpace α)
u₂ : UniformSpace β
u : UniformSpace α
h₁ : u ∈ u₁
hf : UniformContinuous f
⊢ UniformContinuous f
[PROOFSTEP]
delta UniformContinuous
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u₁ : Set (UniformSpace α)
u₂ : UniformSpace β
u : UniformSpace α
h₁ : u ∈ u₁
hf : UniformContinuous f
⊢ Tendsto (fun x => (f x.fst, f x.snd)) (𝓤 α) (𝓤 β)
[PROOFSTEP]
rw [sInf_eq_iInf', iInf_uniformity]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u₁ : Set (UniformSpace α)
u₂ : UniformSpace β
u : UniformSpace α
h₁ : u ∈ u₁
hf : UniformContinuous f
⊢ Tendsto (fun x => (f x.fst, f x.snd)) (⨅ (i : ↑u₁), 𝓤 α) (𝓤 β)
[PROOFSTEP]
exact tendsto_iInf' ⟨u, h₁⟩ hf
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u₁ : UniformSpace α
u₂ : Set (UniformSpace β)
⊢ UniformContinuous f ↔ ∀ (u : UniformSpace β), u ∈ u₂ → UniformContinuous f
[PROOFSTEP]
delta UniformContinuous
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u₁ : UniformSpace α
u₂ : Set (UniformSpace β)
⊢ Tendsto (fun x => (f x.fst, f x.snd)) (𝓤 α) (𝓤 β) ↔
    ∀ (u : UniformSpace β), u ∈ u₂ → Tendsto (fun x => (f x.fst, f x.snd)) (𝓤 α) (𝓤 β)
[PROOFSTEP]
rw [sInf_eq_iInf', iInf_uniformity, tendsto_iInf, SetCoe.forall]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u₁ : ι → UniformSpace α
u₂ : UniformSpace β
i : ι
hf : UniformContinuous f
⊢ UniformContinuous f
[PROOFSTEP]
delta UniformContinuous
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u₁ : ι → UniformSpace α
u₂ : UniformSpace β
i : ι
hf : UniformContinuous f
⊢ Tendsto (fun x => (f x.fst, f x.snd)) (𝓤 α) (𝓤 β)
[PROOFSTEP]
rw [iInf_uniformity]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u₁ : ι → UniformSpace α
u₂ : UniformSpace β
i : ι
hf : UniformContinuous f
⊢ Tendsto (fun x => (f x.fst, f x.snd)) (⨅ (i : ι), 𝓤 α) (𝓤 β)
[PROOFSTEP]
exact tendsto_iInf' i hf
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u₁ : UniformSpace α
u₂ : ι → UniformSpace β
⊢ UniformContinuous f ↔ ∀ (i : ι), UniformContinuous f
[PROOFSTEP]
delta UniformContinuous
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u₁ : UniformSpace α
u₂ : ι → UniformSpace β
⊢ Tendsto (fun x => (f x.fst, f x.snd)) (𝓤 α) (𝓤 β) ↔ ∀ (i : ι), Tendsto (fun x => (f x.fst, f x.snd)) (𝓤 α) (𝓤 β)
[PROOFSTEP]
rw [iInf_uniformity, tendsto_iInf]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
s : Set α
inst✝ : UniformSpace α
⊢ map (Prod.map Subtype.val Subtype.val) (𝓤 ↑s) = 𝓤 α ⊓ 𝓟 (s ×ˢ s)
[PROOFSTEP]
rw [uniformity_setCoe, map_comap, range_prod_map, Subtype.range_val]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
⊢ UniformContinuousOn f s ↔ UniformContinuous (restrict s f)
[PROOFSTEP]
delta UniformContinuousOn UniformContinuous
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
⊢ Tendsto (fun x => (f x.fst, f x.snd)) (𝓤 α ⊓ 𝓟 (s ×ˢ s)) (𝓤 β) ↔
    Tendsto (fun x => (restrict s f x.fst, restrict s f x.snd)) (𝓤 ↑s) (𝓤 β)
[PROOFSTEP]
rw [← map_uniformity_set_coe, tendsto_map'_iff]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
⊢ Tendsto ((fun x => (f x.fst, f x.snd)) ∘ Prod.map Subtype.val Subtype.val) (𝓤 ↑s) (𝓤 β) ↔
    Tendsto (fun x => (restrict s f x.fst, restrict s f x.snd)) (𝓤 ↑s) (𝓤 β)
[PROOFSTEP]
rfl
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
a : α
hf : UniformContinuous fun x => f ↑x
ha : s ∈ 𝓝 a
⊢ Tendsto f (𝓝 a) (𝓝 (f a))
[PROOFSTEP]
rw [(@map_nhds_subtype_coe_eq_nhds α _ s a (mem_of_mem_nhds ha) ha).symm]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
a : α
hf : UniformContinuous fun x => f ↑x
ha : s ∈ 𝓝 a
⊢ Tendsto f (map Subtype.val (𝓝 { val := a, property := (_ : a ∈ s) })) (𝓝 (f a))
[PROOFSTEP]
exact tendsto_map' hf.continuous.continuousAt
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
h : UniformContinuousOn f s
⊢ ContinuousOn f s
[PROOFSTEP]
rw [uniformContinuousOn_iff_restrict] at h 
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
h : UniformContinuous (restrict s f)
⊢ ContinuousOn f s
[PROOFSTEP]
rw [continuousOn_iff_continuous_restrict]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
h : UniformContinuous (restrict s f)
⊢ Continuous (restrict s f)
[PROOFSTEP]
exact h.continuous
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
⊢ comap (fun p => (MulOpposite.op p.fst, MulOpposite.op p.snd)) (𝓤 αᵐᵒᵖ) = 𝓤 α
[PROOFSTEP]
simpa [uniformity_mulOpposite, comap_comap, (· ∘ ·)] using comap_id
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
⊢ 𝓤 (α × β) = comap (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) (𝓤 α ×ˢ 𝓤 β)
[PROOFSTEP]
dsimp [SProd.sprod]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
⊢ 𝓤 (α × β) = comap (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) (Filter.prod (𝓤 α) (𝓤 β))
[PROOFSTEP]
rw [uniformity_prod, Filter.prod, comap_inf, comap_comap, comap_comap]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
⊢ comap (fun p => (p.fst.fst, p.snd.fst)) (𝓤 α) ⊓ comap (fun p => (p.fst.snd, p.snd.snd)) (𝓤 β) =
    comap (Prod.fst ∘ fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) (𝓤 α) ⊓
      comap (Prod.snd ∘ fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) (𝓤 β)
[PROOFSTEP]
rfl
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
⊢ 𝓤 (α × β) = map (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) (𝓤 α ×ˢ 𝓤 β)
[PROOFSTEP]
rw [map_swap4_eq_comap, uniformity_prod_eq_comap_prod]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (β × β)
f : α → α → β
hf : UniformContinuous fun p => f p.fst p.snd
hs : s ∈ 𝓤 β
⊢ ∃ u, u ∈ 𝓤 α ∧ ∀ (a b c : α), (a, b) ∈ u → (f a c, f b c) ∈ s
[PROOFSTEP]
rw [UniformContinuous, uniformity_prod_eq_prod, tendsto_map'_iff] at hf 
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (β × β)
f : α → α → β
hf :
  Tendsto
    ((fun x => (f x.fst.fst x.fst.snd, f x.snd.fst x.snd.snd)) ∘ fun p =>
      ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd))
    (𝓤 α ×ˢ 𝓤 α) (𝓤 β)
hs : s ∈ 𝓤 β
⊢ ∃ u, u ∈ 𝓤 α ∧ ∀ (a b c : α), (a, b) ∈ u → (f a c, f b c) ∈ s
[PROOFSTEP]
rcases mem_prod_iff.1 (mem_map.1 <| hf hs) with ⟨u, hu, v, hv, huvt⟩
[GOAL]
case intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (β × β)
f : α → α → β
hf :
  Tendsto
    ((fun x => (f x.fst.fst x.fst.snd, f x.snd.fst x.snd.snd)) ∘ fun p =>
      ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd))
    (𝓤 α ×ˢ 𝓤 α) (𝓤 β)
hs : s ∈ 𝓤 β
u : Set (α × α)
hu : u ∈ 𝓤 α
v : Set (α × α)
hv : v ∈ 𝓤 α
huvt :
  u ×ˢ v ⊆
    ((fun x => (f x.fst.fst x.fst.snd, f x.snd.fst x.snd.snd)) ∘ fun p =>
        ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹'
      s
⊢ ∃ u, u ∈ 𝓤 α ∧ ∀ (a b c : α), (a, b) ∈ u → (f a c, f b c) ∈ s
[PROOFSTEP]
exact ⟨u, hu, fun a b c hab => @huvt ((_, _), (_, _)) ⟨hab, refl_mem_uniformity hv⟩⟩
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
t₁ : UniformSpace α
t₂ : UniformSpace β
a : Set (α × α)
b : Set (β × β)
ha : a ∈ 𝓤 α
hb : b ∈ 𝓤 β
⊢ {p | (p.fst.fst, p.snd.fst) ∈ a ∧ (p.fst.snd, p.snd.snd) ∈ b} ∈ 𝓤 (α × β)
[PROOFSTEP]
rw [uniformity_prod]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
t₁ : UniformSpace α
t₂ : UniformSpace β
a : Set (α × α)
b : Set (β × β)
ha : a ∈ 𝓤 α
hb : b ∈ 𝓤 β
⊢ {p | (p.fst.fst, p.snd.fst) ∈ a ∧ (p.fst.snd, p.snd.snd) ∈ b} ∈
    comap (fun p => (p.fst.fst, p.snd.fst)) (𝓤 α) ⊓ comap (fun p => (p.fst.snd, p.snd.snd)) (𝓤 β)
[PROOFSTEP]
exact inter_mem_inf (preimage_mem_comap ha) (preimage_mem_comap hb)
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f₁ : α → β
f₂ : α → γ
h₁ : UniformContinuous f₁
h₂ : UniformContinuous f₂
⊢ UniformContinuous fun a => (f₁ a, f₂ a)
[PROOFSTEP]
rw [UniformContinuous, uniformity_prod]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f₁ : α → β
f₂ : α → γ
h₁ : UniformContinuous f₁
h₂ : UniformContinuous f₂
⊢ Tendsto (fun x => ((f₁ x.fst, f₂ x.fst), f₁ x.snd, f₂ x.snd)) (𝓤 α)
    (comap (fun p => (p.fst.fst, p.snd.fst)) (𝓤 β) ⊓ comap (fun p => (p.fst.snd, p.snd.snd)) (𝓤 γ))
[PROOFSTEP]
exact tendsto_inf.2 ⟨tendsto_comap_iff.2 h₁, tendsto_comap_iff.2 h₂⟩
[GOAL]
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type ?u.174697
β : Type ?u.174703
γ : Type ?u.174709
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
⊢ Sort ?u.174711
[PROOFSTEP]
haveI := ua1
[GOAL]
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type ?u.174697
β : Type ?u.174703
γ : Type ?u.174709
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
this : UniformSpace α
⊢ Sort ?u.174711
[PROOFSTEP]
haveI := ub1
[GOAL]
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type ?u.174697
β : Type ?u.174703
γ : Type ?u.174709
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
this✝ : UniformSpace α
this : UniformSpace β
⊢ Sort ?u.174711
[PROOFSTEP]
exact UniformContinuous fun p : α × β => f p.1 p.2
[GOAL]
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type ?u.174697
β : Type ?u.174703
γ : Type ?u.174709
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous fun p => f p.fst p.snd
⊢ Sort ?u.174714
[PROOFSTEP]
haveI := ua1 ⊓ ua2
[GOAL]
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type ?u.174697
β : Type ?u.174703
γ : Type ?u.174709
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous fun p => f p.fst p.snd
this : UniformSpace α
⊢ Sort ?u.174714
[PROOFSTEP]
haveI := ub1 ⊓ ub2
[GOAL]
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type ?u.174697
β : Type ?u.174703
γ : Type ?u.174709
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous fun p => f p.fst p.snd
this✝ : UniformSpace α
this : UniformSpace β
⊢ Sort ?u.174714
[PROOFSTEP]
exact UniformContinuous fun p : α × β => f p.1 p.2
[GOAL]
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous fun p => f p.fst p.snd
⊢ UniformContinuous fun p => f p.fst p.snd
[PROOFSTEP]
have ha := @UniformContinuous.inf_dom_left _ _ id ua1 ua2 ua1 (@uniformContinuous_id _ (id _))
[GOAL]
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous fun p => f p.fst p.snd
ha : UniformContinuous id
⊢ UniformContinuous fun p => f p.fst p.snd
[PROOFSTEP]
have hb := @UniformContinuous.inf_dom_left _ _ id ub1 ub2 ub1 (@uniformContinuous_id _ (id _))
[GOAL]
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous fun p => f p.fst p.snd
ha : UniformContinuous id
hb : UniformContinuous id
⊢ UniformContinuous fun p => f p.fst p.snd
[PROOFSTEP]
have h_unif_cont_id := @UniformContinuous.prod_map _ _ _ _ (ua1 ⊓ ua2) (ub1 ⊓ ub2) ua1 ub1 _ _ ha hb
[GOAL]
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous fun p => f p.fst p.snd
ha : UniformContinuous id
hb : UniformContinuous id
h_unif_cont_id : UniformContinuous (Prod.map id id)
⊢ UniformContinuous fun p => f p.fst p.snd
[PROOFSTEP]
exact @UniformContinuous.comp _ _ _ (id _) (id _) _ _ _ h h_unif_cont_id
[GOAL]
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type ?u.176203
β : Type ?u.176209
γ : Type ?u.176215
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
⊢ Sort ?u.176217
[PROOFSTEP]
haveI := ua2
[GOAL]
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type ?u.176203
β : Type ?u.176209
γ : Type ?u.176215
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
this : UniformSpace α
⊢ Sort ?u.176217
[PROOFSTEP]
haveI := ub2
[GOAL]
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type ?u.176203
β : Type ?u.176209
γ : Type ?u.176215
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
this✝ : UniformSpace α
this : UniformSpace β
⊢ Sort ?u.176217
[PROOFSTEP]
exact UniformContinuous fun p : α × β => f p.1 p.2
[GOAL]
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type ?u.176203
β : Type ?u.176209
γ : Type ?u.176215
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous fun p => f p.fst p.snd
⊢ Sort ?u.176220
[PROOFSTEP]
haveI := ua1 ⊓ ua2
[GOAL]
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type ?u.176203
β : Type ?u.176209
γ : Type ?u.176215
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous fun p => f p.fst p.snd
this : UniformSpace α
⊢ Sort ?u.176220
[PROOFSTEP]
haveI := ub1 ⊓ ub2
[GOAL]
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type ?u.176203
β : Type ?u.176209
γ : Type ?u.176215
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous fun p => f p.fst p.snd
this✝ : UniformSpace α
this : UniformSpace β
⊢ Sort ?u.176220
[PROOFSTEP]
exact UniformContinuous fun p : α × β => f p.1 p.2
[GOAL]
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous fun p => f p.fst p.snd
⊢ UniformContinuous fun p => f p.fst p.snd
[PROOFSTEP]
have ha := @UniformContinuous.inf_dom_right _ _ id ua1 ua2 ua2 (@uniformContinuous_id _ (id _))
[GOAL]
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous fun p => f p.fst p.snd
ha : UniformContinuous id
⊢ UniformContinuous fun p => f p.fst p.snd
[PROOFSTEP]
have hb := @UniformContinuous.inf_dom_right _ _ id ub1 ub2 ub2 (@uniformContinuous_id _ (id _))
[GOAL]
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous fun p => f p.fst p.snd
ha : UniformContinuous id
hb : UniformContinuous id
⊢ UniformContinuous fun p => f p.fst p.snd
[PROOFSTEP]
have h_unif_cont_id := @UniformContinuous.prod_map _ _ _ _ (ua1 ⊓ ua2) (ub1 ⊓ ub2) ua2 ub2 _ _ ha hb
[GOAL]
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous fun p => f p.fst p.snd
ha : UniformContinuous id
hb : UniformContinuous id
h_unif_cont_id : UniformContinuous (Prod.map id id)
⊢ UniformContinuous fun p => f p.fst p.snd
[PROOFSTEP]
exact @UniformContinuous.comp _ _ _ (id _) (id _) _ _ _ h h_unif_cont_id
[GOAL]
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type ?u.177710
β : Type ?u.177714
γ : Type ?u.177723
f : α → β → γ
uas : Set (UniformSpace α)
ubs : Set (UniformSpace β)
ua : UniformSpace α
ub : UniformSpace β
uc : UniformSpace γ
ha : ua ∈ uas
hb : ub ∈ ubs
hf : UniformContinuous fun p => f p.fst p.snd
⊢ Sort ?u.177870
[PROOFSTEP]
haveI := sInf uas
[GOAL]
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type ?u.177710
β : Type ?u.177714
γ : Type ?u.177723
f : α → β → γ
uas : Set (UniformSpace α)
ubs : Set (UniformSpace β)
ua : UniformSpace α
ub : UniformSpace β
uc : UniformSpace γ
ha : ua ∈ uas
hb : ub ∈ ubs
hf : UniformContinuous fun p => f p.fst p.snd
this : UniformSpace α
⊢ Sort ?u.177870
[PROOFSTEP]
haveI := sInf ubs
[GOAL]
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type ?u.177710
β : Type ?u.177714
γ : Type ?u.177723
f : α → β → γ
uas : Set (UniformSpace α)
ubs : Set (UniformSpace β)
ua : UniformSpace α
ub : UniformSpace β
uc : UniformSpace γ
ha : ua ∈ uas
hb : ub ∈ ubs
hf : UniformContinuous fun p => f p.fst p.snd
this✝ : UniformSpace α
this : UniformSpace β
⊢ Sort ?u.177870
[PROOFSTEP]
exact @UniformContinuous _ _ _ uc fun p : α × β => f p.1 p.2
[GOAL]
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
uas : Set (UniformSpace α)
ubs : Set (UniformSpace β)
ua : UniformSpace α
ub : UniformSpace β
uc : UniformSpace γ
ha : ua ∈ uas
hb : ub ∈ ubs
hf : UniformContinuous fun p => f p.fst p.snd
⊢ UniformContinuous fun p => f p.fst p.snd
[PROOFSTEP]
let _ : UniformSpace (α × β) := instUniformSpaceProd
[GOAL]
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
uas : Set (UniformSpace α)
ubs : Set (UniformSpace β)
ua : UniformSpace α
ub : UniformSpace β
uc : UniformSpace γ
ha : ua ∈ uas
hb : ub ∈ ubs
hf : UniformContinuous fun p => f p.fst p.snd
x✝ : UniformSpace (α × β) := instUniformSpaceProd
⊢ UniformContinuous fun p => f p.fst p.snd
[PROOFSTEP]
have ha := uniformContinuous_sInf_dom ha uniformContinuous_id
[GOAL]
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
uas : Set (UniformSpace α)
ubs : Set (UniformSpace β)
ua : UniformSpace α
ub : UniformSpace β
uc : UniformSpace γ
ha✝ : ua ∈ uas
hb : ub ∈ ubs
hf : UniformContinuous fun p => f p.fst p.snd
x✝ : UniformSpace (α × β) := instUniformSpaceProd
ha : UniformContinuous id
⊢ UniformContinuous fun p => f p.fst p.snd
[PROOFSTEP]
have hb := uniformContinuous_sInf_dom hb uniformContinuous_id
[GOAL]
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
uas : Set (UniformSpace α)
ubs : Set (UniformSpace β)
ua : UniformSpace α
ub : UniformSpace β
uc : UniformSpace γ
ha✝ : ua ∈ uas
hb✝ : ub ∈ ubs
hf : UniformContinuous fun p => f p.fst p.snd
x✝ : UniformSpace (α × β) := instUniformSpaceProd
ha : UniformContinuous id
hb : UniformContinuous id
⊢ UniformContinuous fun p => f p.fst p.snd
[PROOFSTEP]
have h_unif_cont_id := @UniformContinuous.prod_map _ _ _ _ (sInf uas) (sInf ubs) ua ub _ _ ha hb
[GOAL]
α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
uas : Set (UniformSpace α)
ubs : Set (UniformSpace β)
ua : UniformSpace α
ub : UniformSpace β
uc : UniformSpace γ
ha✝ : ua ∈ uas
hb✝ : ub ∈ ubs
hf : UniformContinuous fun p => f p.fst p.snd
x✝ : UniformSpace (α × β) := instUniformSpaceProd
ha : UniformContinuous id
hb : UniformContinuous id
h_unif_cont_id : UniformContinuous (Prod.map id id)
⊢ UniformContinuous fun p => f p.fst p.snd
[PROOFSTEP]
exact @UniformContinuous.comp _ _ _ (id _) (id _) _ _ _ hf h_unif_cont_id
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
δ' : Type u_2
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : UniformSpace γ
inst✝¹ : UniformSpace δ
inst✝ : UniformSpace δ'
f : α × β → γ
⊢ UniformContinuous₂ (curry f) ↔ UniformContinuous f
[PROOFSTEP]
rw [UniformContinuous₂, uncurry_curry]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set ((α ⊕ β) × (α ⊕ β))
x✝ : r ∈ map (fun p => (inl p.fst, inl p.snd)) (𝓤 α) ⊔ map (fun p => (inr p.fst, inr p.snd)) (𝓤 β)
x : α ⊕ β
H₁ : r ∈ (map (fun p => (inl p.fst, inl p.snd)) (𝓤 α)).sets
H₂ : r ∈ (map (fun p => (inr p.fst, inr p.snd)) (𝓤 β)).sets
⊢ (x, x) ∈ r
[PROOFSTEP]
cases x <;> [apply refl_mem_uniformity H₁; apply refl_mem_uniformity H₂]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set ((α ⊕ β) × (α ⊕ β))
x✝ : r ∈ map (fun p => (inl p.fst, inl p.snd)) (𝓤 α) ⊔ map (fun p => (inr p.fst, inr p.snd)) (𝓤 β)
x : α ⊕ β
H₁ : r ∈ (map (fun p => (inl p.fst, inl p.snd)) (𝓤 α)).sets
H₂ : r ∈ (map (fun p => (inr p.fst, inr p.snd)) (𝓤 β)).sets
⊢ (x, x) ∈ r
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set ((α ⊕ β) × (α ⊕ β))
x✝ : r ∈ map (fun p => (inl p.fst, inl p.snd)) (𝓤 α) ⊔ map (fun p => (inr p.fst, inr p.snd)) (𝓤 β)
H₁ : r ∈ (map (fun p => (inl p.fst, inl p.snd)) (𝓤 α)).sets
H₂ : r ∈ (map (fun p => (inr p.fst, inr p.snd)) (𝓤 β)).sets
val✝ : α
⊢ (inl val✝, inl val✝) ∈ r
[PROOFSTEP]
apply refl_mem_uniformity H₁
[GOAL]
case inr
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set ((α ⊕ β) × (α ⊕ β))
x✝ : r ∈ map (fun p => (inl p.fst, inl p.snd)) (𝓤 α) ⊔ map (fun p => (inr p.fst, inr p.snd)) (𝓤 β)
H₁ : r ∈ (map (fun p => (inl p.fst, inl p.snd)) (𝓤 α)).sets
H₂ : r ∈ (map (fun p => (inr p.fst, inr p.snd)) (𝓤 β)).sets
val✝ : β
⊢ (inr val✝, inr val✝) ∈ r
[PROOFSTEP]
apply refl_mem_uniformity H₂
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set ((α ⊕ β) × (α ⊕ β))
x✝ : r ∈ map (fun p => (inl p.fst, inl p.snd)) (𝓤 α) ⊔ map (fun p => (inr p.fst, inr p.snd)) (𝓤 β)
Hrα : r ∈ (map (fun p => (inl p.fst, inl p.snd)) (𝓤 α)).sets
Hrβ : r ∈ (map (fun p => (inr p.fst, inr p.snd)) (𝓤 β)).sets
⊢ ∃ t, t ∈ map (fun p => (inl p.fst, inl p.snd)) (𝓤 α) ⊔ map (fun p => (inr p.fst, inr p.snd)) (𝓤 β) ∧ t ○ t ⊆ r
[PROOFSTEP]
rcases comp_mem_uniformity_sets Hrα with ⟨tα, htα, Htα⟩
[GOAL]
case intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set ((α ⊕ β) × (α ⊕ β))
x✝ : r ∈ map (fun p => (inl p.fst, inl p.snd)) (𝓤 α) ⊔ map (fun p => (inr p.fst, inr p.snd)) (𝓤 β)
Hrα : r ∈ (map (fun p => (inl p.fst, inl p.snd)) (𝓤 α)).sets
Hrβ : r ∈ (map (fun p => (inr p.fst, inr p.snd)) (𝓤 β)).sets
tα : Set (α × α)
htα : tα ∈ 𝓤 α
Htα : tα ○ tα ⊆ (fun p => (inl p.fst, inl p.snd)) ⁻¹' r
⊢ ∃ t, t ∈ map (fun p => (inl p.fst, inl p.snd)) (𝓤 α) ⊔ map (fun p => (inr p.fst, inr p.snd)) (𝓤 β) ∧ t ○ t ⊆ r
[PROOFSTEP]
rcases comp_mem_uniformity_sets Hrβ with ⟨tβ, htβ, Htβ⟩
[GOAL]
case intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set ((α ⊕ β) × (α ⊕ β))
x✝ : r ∈ map (fun p => (inl p.fst, inl p.snd)) (𝓤 α) ⊔ map (fun p => (inr p.fst, inr p.snd)) (𝓤 β)
Hrα : r ∈ (map (fun p => (inl p.fst, inl p.snd)) (𝓤 α)).sets
Hrβ : r ∈ (map (fun p => (inr p.fst, inr p.snd)) (𝓤 β)).sets
tα : Set (α × α)
htα : tα ∈ 𝓤 α
Htα : tα ○ tα ⊆ (fun p => (inl p.fst, inl p.snd)) ⁻¹' r
tβ : Set (β × β)
htβ : tβ ∈ 𝓤 β
Htβ : tβ ○ tβ ⊆ (fun p => (inr p.fst, inr p.snd)) ⁻¹' r
⊢ ∃ t, t ∈ map (fun p => (inl p.fst, inl p.snd)) (𝓤 α) ⊔ map (fun p => (inr p.fst, inr p.snd)) (𝓤 β) ∧ t ○ t ⊆ r
[PROOFSTEP]
refine'
  ⟨_,
    ⟨mem_map_iff_exists_image.2 ⟨tα, htα, subset_union_left _ _⟩,
      mem_map_iff_exists_image.2 ⟨tβ, htβ, subset_union_right _ _⟩⟩,
    _⟩
[GOAL]
case intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set ((α ⊕ β) × (α ⊕ β))
x✝ : r ∈ map (fun p => (inl p.fst, inl p.snd)) (𝓤 α) ⊔ map (fun p => (inr p.fst, inr p.snd)) (𝓤 β)
Hrα : r ∈ (map (fun p => (inl p.fst, inl p.snd)) (𝓤 α)).sets
Hrβ : r ∈ (map (fun p => (inr p.fst, inr p.snd)) (𝓤 β)).sets
tα : Set (α × α)
htα : tα ∈ 𝓤 α
Htα : tα ○ tα ⊆ (fun p => (inl p.fst, inl p.snd)) ⁻¹' r
tβ : Set (β × β)
htβ : tβ ∈ 𝓤 β
Htβ : tβ ○ tβ ⊆ (fun p => (inr p.fst, inr p.snd)) ⁻¹' r
⊢ (fun p => (inl p.fst, inl p.snd)) '' tα ∪ (fun p => (inr p.fst, inr p.snd)) '' tβ ○
      (fun p => (inl p.fst, inl p.snd)) '' tα ∪ (fun p => (inr p.fst, inr p.snd)) '' tβ ⊆
    r
[PROOFSTEP]
rintro ⟨_, _⟩ ⟨z, ⟨⟨a, b⟩, hab, ⟨⟩⟩ | ⟨⟨a, b⟩, hab, ⟨⟩⟩, ⟨⟨_, c⟩, hbc, ⟨⟩⟩ | ⟨⟨_, c⟩, hbc, ⟨⟩⟩⟩
[GOAL]
case intro.intro.intro.intro.mk.intro.intro.inl.intro.mk.intro.refl.inl.intro.mk.intro.refl
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set ((α ⊕ β) × (α ⊕ β))
x✝ : r ∈ map (fun p => (inl p.fst, inl p.snd)) (𝓤 α) ⊔ map (fun p => (inr p.fst, inr p.snd)) (𝓤 β)
Hrα : r ∈ (map (fun p => (inl p.fst, inl p.snd)) (𝓤 α)).sets
Hrβ : r ∈ (map (fun p => (inr p.fst, inr p.snd)) (𝓤 β)).sets
tα : Set (α × α)
htα : tα ∈ 𝓤 α
Htα : tα ○ tα ⊆ (fun p => (inl p.fst, inl p.snd)) ⁻¹' r
tβ : Set (β × β)
htβ : tβ ∈ 𝓤 β
Htβ : tβ ○ tβ ⊆ (fun p => (inr p.fst, inr p.snd)) ⁻¹' r
a b : α
hab : (a, b) ∈ tα
c : α
hbc : (b, c) ∈ tα
⊢ (inl (a, b).fst, inl (b, c).snd) ∈ r
[PROOFSTEP]
have A : (a, c) ∈ tα ○ tα := ⟨b, hab, hbc⟩
[GOAL]
case intro.intro.intro.intro.mk.intro.intro.inl.intro.mk.intro.refl.inl.intro.mk.intro.refl
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set ((α ⊕ β) × (α ⊕ β))
x✝ : r ∈ map (fun p => (inl p.fst, inl p.snd)) (𝓤 α) ⊔ map (fun p => (inr p.fst, inr p.snd)) (𝓤 β)
Hrα : r ∈ (map (fun p => (inl p.fst, inl p.snd)) (𝓤 α)).sets
Hrβ : r ∈ (map (fun p => (inr p.fst, inr p.snd)) (𝓤 β)).sets
tα : Set (α × α)
htα : tα ∈ 𝓤 α
Htα : tα ○ tα ⊆ (fun p => (inl p.fst, inl p.snd)) ⁻¹' r
tβ : Set (β × β)
htβ : tβ ∈ 𝓤 β
Htβ : tβ ○ tβ ⊆ (fun p => (inr p.fst, inr p.snd)) ⁻¹' r
a b : α
hab : (a, b) ∈ tα
c : α
hbc : (b, c) ∈ tα
A : (a, c) ∈ tα ○ tα
⊢ (inl (a, b).fst, inl (b, c).snd) ∈ r
[PROOFSTEP]
exact Htα A
[GOAL]
case intro.intro.intro.intro.mk.intro.intro.inr.intro.mk.intro.refl.inr.intro.mk.intro.refl
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set ((α ⊕ β) × (α ⊕ β))
x✝ : r ∈ map (fun p => (inl p.fst, inl p.snd)) (𝓤 α) ⊔ map (fun p => (inr p.fst, inr p.snd)) (𝓤 β)
Hrα : r ∈ (map (fun p => (inl p.fst, inl p.snd)) (𝓤 α)).sets
Hrβ : r ∈ (map (fun p => (inr p.fst, inr p.snd)) (𝓤 β)).sets
tα : Set (α × α)
htα : tα ∈ 𝓤 α
Htα : tα ○ tα ⊆ (fun p => (inl p.fst, inl p.snd)) ⁻¹' r
tβ : Set (β × β)
htβ : tβ ∈ 𝓤 β
Htβ : tβ ○ tβ ⊆ (fun p => (inr p.fst, inr p.snd)) ⁻¹' r
a b : β
hab : (a, b) ∈ tβ
c : β
hbc : (b, c) ∈ tβ
⊢ (inr (a, b).fst, inr (b, c).snd) ∈ r
[PROOFSTEP]
have A : (a, c) ∈ tβ ○ tβ := ⟨b, hab, hbc⟩
[GOAL]
case intro.intro.intro.intro.mk.intro.intro.inr.intro.mk.intro.refl.inr.intro.mk.intro.refl
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set ((α ⊕ β) × (α ⊕ β))
x✝ : r ∈ map (fun p => (inl p.fst, inl p.snd)) (𝓤 α) ⊔ map (fun p => (inr p.fst, inr p.snd)) (𝓤 β)
Hrα : r ∈ (map (fun p => (inl p.fst, inl p.snd)) (𝓤 α)).sets
Hrβ : r ∈ (map (fun p => (inr p.fst, inr p.snd)) (𝓤 β)).sets
tα : Set (α × α)
htα : tα ∈ 𝓤 α
Htα : tα ○ tα ⊆ (fun p => (inl p.fst, inl p.snd)) ⁻¹' r
tβ : Set (β × β)
htβ : tβ ∈ 𝓤 β
Htβ : tβ ○ tβ ⊆ (fun p => (inr p.fst, inr p.snd)) ⁻¹' r
a b : β
hab : (a, b) ∈ tβ
c : β
hbc : (b, c) ∈ tβ
A : (a, c) ∈ tβ ○ tβ
⊢ (inr (a, b).fst, inr (b, c).snd) ∈ r
[PROOFSTEP]
exact Htβ A
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : IsOpen s
x : α ⊕ β
xs : x ∈ s
⊢ {p | p.fst = x → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : IsOpen s
val✝ : α
xs : inl val✝ ∈ s
⊢ {p | p.fst = inl val✝ → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
[PROOFSTEP]
refine'
  mem_of_superset (union_mem_uniformity_sum (mem_nhds_uniformity_iff_right.1 (hs.1.mem_nhds xs)) univ_mem)
    (union_subset _ _)
[GOAL]
case inl.refine'_1
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : IsOpen s
val✝ : α
xs : inl val✝ ∈ s
⊢ (fun p => (inl p.fst, inl p.snd)) '' {p | p.fst = val✝ → p.snd ∈ inl ⁻¹' s} ⊆ {p | p.fst = inl val✝ → p.snd ∈ s}
[PROOFSTEP]
rintro _ ⟨⟨_, b⟩, h, ⟨⟩⟩ ⟨⟩
[GOAL]
case inl.refine'_2
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : IsOpen s
val✝ : α
xs : inl val✝ ∈ s
⊢ (fun p => (inr p.fst, inr p.snd)) '' univ ⊆ {p | p.fst = inl val✝ → p.snd ∈ s}
[PROOFSTEP]
rintro _ ⟨⟨_, b⟩, h, ⟨⟩⟩ ⟨⟩
[GOAL]
case inl.refine'_1.intro.mk.intro.refl.refl
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : IsOpen s
fst✝ b : α
xs : inl (fst✝, b).fst ∈ s
h : (fst✝, b) ∈ {p | p.fst = (fst✝, b).fst → p.snd ∈ inl ⁻¹' s}
⊢ ((fun p => (inl p.fst, inl p.snd)) (fst✝, b)).snd ∈ s
[PROOFSTEP]
exact h rfl
[GOAL]
case inr
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : IsOpen s
val✝ : β
xs : inr val✝ ∈ s
⊢ {p | p.fst = inr val✝ → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
[PROOFSTEP]
refine'
  mem_of_superset (union_mem_uniformity_sum univ_mem (mem_nhds_uniformity_iff_right.1 (hs.2.mem_nhds xs)))
    (union_subset _ _)
[GOAL]
case inr.refine'_1
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : IsOpen s
val✝ : β
xs : inr val✝ ∈ s
⊢ (fun p => (inl p.fst, inl p.snd)) '' univ ⊆ {p | p.fst = inr val✝ → p.snd ∈ s}
[PROOFSTEP]
rintro _ ⟨⟨a, _⟩, h, ⟨⟩⟩ ⟨⟩
[GOAL]
case inr.refine'_2
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : IsOpen s
val✝ : β
xs : inr val✝ ∈ s
⊢ (fun p => (inr p.fst, inr p.snd)) '' {p | p.fst = val✝ → p.snd ∈ inr ⁻¹' s} ⊆ {p | p.fst = inr val✝ → p.snd ∈ s}
[PROOFSTEP]
rintro _ ⟨⟨a, _⟩, h, ⟨⟩⟩ ⟨⟩
[GOAL]
case inr.refine'_2.intro.mk.intro.refl.refl
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : IsOpen s
a snd✝ : β
xs : inr (a, snd✝).fst ∈ s
h : (a, snd✝) ∈ {p | p.fst = (a, snd✝).fst → p.snd ∈ inr ⁻¹' s}
⊢ ((fun p => (inr p.fst, inr p.snd)) (a, snd✝)).snd ∈ s
[PROOFSTEP]
exact h rfl
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : ∀ (x : α ⊕ β), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
⊢ IsOpen s
[PROOFSTEP]
constructor
[GOAL]
case left
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : ∀ (x : α ⊕ β), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
⊢ s ∈
    (↑OrderDual.toDual ∘ (fun t => ↑OrderDual.toDual {s | IsOpen s}) ∘ ↑OrderDual.ofDual)
      (TopologicalSpace.coinduced inl UniformSpace.toTopologicalSpace)
[PROOFSTEP]
refine' (@isOpen_iff_mem_nhds α _ _).2 fun a ha => mem_nhds_uniformity_iff_right.2 _
[GOAL]
case left
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : ∀ (x : α ⊕ β), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
a : α
ha : a ∈ inl ⁻¹' s
⊢ {p | p.fst = a → p.snd ∈ inl ⁻¹' s} ∈ 𝓤 α
[PROOFSTEP]
rcases mem_map_iff_exists_image.1 (hs _ ha).1 with ⟨t, ht, st⟩
[GOAL]
case left.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : ∀ (x : α ⊕ β), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
a : α
ha : a ∈ inl ⁻¹' s
t : Set (α × α)
ht : t ∈ 𝓤 α
st : (fun p => (inl p.fst, inl p.snd)) '' t ⊆ {p | p.fst = inl a → p.snd ∈ s}
⊢ {p | p.fst = a → p.snd ∈ inl ⁻¹' s} ∈ 𝓤 α
[PROOFSTEP]
refine' mem_of_superset ht _
[GOAL]
case left.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : ∀ (x : α ⊕ β), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
a : α
ha : a ∈ inl ⁻¹' s
t : Set (α × α)
ht : t ∈ 𝓤 α
st : (fun p => (inl p.fst, inl p.snd)) '' t ⊆ {p | p.fst = inl a → p.snd ∈ s}
⊢ t ⊆ {p | p.fst = a → p.snd ∈ inl ⁻¹' s}
[PROOFSTEP]
rintro p pt rfl
[GOAL]
case left.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : ∀ (x : α ⊕ β), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
t : Set (α × α)
ht : t ∈ 𝓤 α
p : α × α
pt : p ∈ t
ha : p.fst ∈ inl ⁻¹' s
st : (fun p => (inl p.fst, inl p.snd)) '' t ⊆ {p_1 | p_1.fst = inl p.fst → p_1.snd ∈ s}
⊢ p.snd ∈ inl ⁻¹' s
[PROOFSTEP]
exact st ⟨_, pt, rfl⟩ rfl
[GOAL]
case right
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : ∀ (x : α ⊕ β), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
⊢ s ∈
    (↑OrderDual.toDual ∘ (fun t => ↑OrderDual.toDual {s | IsOpen s}) ∘ ↑OrderDual.ofDual)
      (TopologicalSpace.coinduced inr UniformSpace.toTopologicalSpace)
[PROOFSTEP]
refine' (@isOpen_iff_mem_nhds β _ _).2 fun b hb => mem_nhds_uniformity_iff_right.2 _
[GOAL]
case right
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : ∀ (x : α ⊕ β), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
b : β
hb : b ∈ inr ⁻¹' s
⊢ {p | p.fst = b → p.snd ∈ inr ⁻¹' s} ∈ 𝓤 β
[PROOFSTEP]
rcases mem_map_iff_exists_image.1 (hs _ hb).2 with ⟨t, ht, st⟩
[GOAL]
case right.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : ∀ (x : α ⊕ β), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
b : β
hb : b ∈ inr ⁻¹' s
t : Set (β × β)
ht : t ∈ 𝓤 β
st : (fun p => (inr p.fst, inr p.snd)) '' t ⊆ {p | p.fst = inr b → p.snd ∈ s}
⊢ {p | p.fst = b → p.snd ∈ inr ⁻¹' s} ∈ 𝓤 β
[PROOFSTEP]
refine' mem_of_superset ht _
[GOAL]
case right.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : ∀ (x : α ⊕ β), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
b : β
hb : b ∈ inr ⁻¹' s
t : Set (β × β)
ht : t ∈ 𝓤 β
st : (fun p => (inr p.fst, inr p.snd)) '' t ⊆ {p | p.fst = inr b → p.snd ∈ s}
⊢ t ⊆ {p | p.fst = b → p.snd ∈ inr ⁻¹' s}
[PROOFSTEP]
rintro p pt rfl
[GOAL]
case right.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : ∀ (x : α ⊕ β), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
t : Set (β × β)
ht : t ∈ 𝓤 β
p : β × β
pt : p ∈ t
hb : p.fst ∈ inr ⁻¹' s
st : (fun p => (inr p.fst, inr p.snd)) '' t ⊆ {p_1 | p_1.fst = inr p.fst → p_1.snd ∈ s}
⊢ p.snd ∈ inr ⁻¹' s
[PROOFSTEP]
exact st ⟨_, pt, rfl⟩ rfl
[GOAL]
α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι✝ : Sort u_1
α : Type u
inst✝ : UniformSpace α
s : Set α
ι : Sort u_2
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : s ⊆ ⋃ (i : ι), c i
⊢ ∃ n, n ∈ 𝓤 α ∧ ∀ (x : α), x ∈ s → ∃ i, {y | (x, y) ∈ n} ⊆ c i
[PROOFSTEP]
let u n := {x | ∃ i, ∃ m ∈ 𝓤 α, {y | (x, y) ∈ m ○ n} ⊆ c i}
[GOAL]
α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι✝ : Sort u_1
α : Type u
inst✝ : UniformSpace α
s : Set α
ι : Sort u_2
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : s ⊆ ⋃ (i : ι), c i
u : Set (α × α) → Set α := fun n => {x | ∃ i m, m ∈ 𝓤 α ∧ {y | (x, y) ∈ m ○ n} ⊆ c i}
⊢ ∃ n, n ∈ 𝓤 α ∧ ∀ (x : α), x ∈ s → ∃ i, {y | (x, y) ∈ n} ⊆ c i
[PROOFSTEP]
have hu₁ : ∀ n ∈ 𝓤 α, IsOpen (u n) := by
  refine' fun n _ => isOpen_uniformity.2 _
  rintro x ⟨i, m, hm, h⟩
  rcases comp_mem_uniformity_sets hm with ⟨m', hm', mm'⟩
  apply (𝓤 α).sets_of_superset hm'
  rintro ⟨x, y⟩ hp rfl
  refine' ⟨i, m', hm', fun z hz => h (monotone_id.compRel monotone_const mm' _)⟩
  dsimp [-mem_compRel] at hz ⊢
  rw [compRel_assoc]
  exact ⟨y, hp, hz⟩
[GOAL]
α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι✝ : Sort u_1
α : Type u
inst✝ : UniformSpace α
s : Set α
ι : Sort u_2
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : s ⊆ ⋃ (i : ι), c i
u : Set (α × α) → Set α := fun n => {x | ∃ i m, m ∈ 𝓤 α ∧ {y | (x, y) ∈ m ○ n} ⊆ c i}
⊢ ∀ (n : Set (α × α)), n ∈ 𝓤 α → IsOpen (u n)
[PROOFSTEP]
refine' fun n _ => isOpen_uniformity.2 _
[GOAL]
α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι✝ : Sort u_1
α : Type u
inst✝ : UniformSpace α
s : Set α
ι : Sort u_2
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : s ⊆ ⋃ (i : ι), c i
u : Set (α × α) → Set α := fun n => {x | ∃ i m, m ∈ 𝓤 α ∧ {y | (x, y) ∈ m ○ n} ⊆ c i}
n : Set (α × α)
x✝ : n ∈ 𝓤 α
⊢ ∀ (x : α), x ∈ u n → {p | p.fst = x → p.snd ∈ u n} ∈ 𝓤 α
[PROOFSTEP]
rintro x ⟨i, m, hm, h⟩
[GOAL]
case intro.intro.intro
α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι✝ : Sort u_1
α : Type u
inst✝ : UniformSpace α
s : Set α
ι : Sort u_2
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : s ⊆ ⋃ (i : ι), c i
u : Set (α × α) → Set α := fun n => {x | ∃ i m, m ∈ 𝓤 α ∧ {y | (x, y) ∈ m ○ n} ⊆ c i}
n : Set (α × α)
x✝ : n ∈ 𝓤 α
x : α
i : ι
m : Set (α × α)
hm : m ∈ 𝓤 α
h : {y | (x, y) ∈ m ○ n} ⊆ c i
⊢ {p | p.fst = x → p.snd ∈ u n} ∈ 𝓤 α
[PROOFSTEP]
rcases comp_mem_uniformity_sets hm with ⟨m', hm', mm'⟩
[GOAL]
case intro.intro.intro.intro.intro
α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι✝ : Sort u_1
α : Type u
inst✝ : UniformSpace α
s : Set α
ι : Sort u_2
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : s ⊆ ⋃ (i : ι), c i
u : Set (α × α) → Set α := fun n => {x | ∃ i m, m ∈ 𝓤 α ∧ {y | (x, y) ∈ m ○ n} ⊆ c i}
n : Set (α × α)
x✝ : n ∈ 𝓤 α
x : α
i : ι
m : Set (α × α)
hm : m ∈ 𝓤 α
h : {y | (x, y) ∈ m ○ n} ⊆ c i
m' : Set (α × α)
hm' : m' ∈ 𝓤 α
mm' : m' ○ m' ⊆ m
⊢ {p | p.fst = x → p.snd ∈ u n} ∈ 𝓤 α
[PROOFSTEP]
apply (𝓤 α).sets_of_superset hm'
[GOAL]
case intro.intro.intro.intro.intro
α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι✝ : Sort u_1
α : Type u
inst✝ : UniformSpace α
s : Set α
ι : Sort u_2
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : s ⊆ ⋃ (i : ι), c i
u : Set (α × α) → Set α := fun n => {x | ∃ i m, m ∈ 𝓤 α ∧ {y | (x, y) ∈ m ○ n} ⊆ c i}
n : Set (α × α)
x✝ : n ∈ 𝓤 α
x : α
i : ι
m : Set (α × α)
hm : m ∈ 𝓤 α
h : {y | (x, y) ∈ m ○ n} ⊆ c i
m' : Set (α × α)
hm' : m' ∈ 𝓤 α
mm' : m' ○ m' ⊆ m
⊢ m' ⊆ {p | p.fst = x → p.snd ∈ u n}
[PROOFSTEP]
rintro ⟨x, y⟩ hp rfl
[GOAL]
case intro.intro.intro.intro.intro.mk
α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι✝ : Sort u_1
α : Type u
inst✝ : UniformSpace α
s : Set α
ι : Sort u_2
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : s ⊆ ⋃ (i : ι), c i
u : Set (α × α) → Set α := fun n => {x | ∃ i m, m ∈ 𝓤 α ∧ {y | (x, y) ∈ m ○ n} ⊆ c i}
n : Set (α × α)
x✝ : n ∈ 𝓤 α
i : ι
m : Set (α × α)
hm : m ∈ 𝓤 α
m' : Set (α × α)
hm' : m' ∈ 𝓤 α
mm' : m' ○ m' ⊆ m
x y : α
hp : (x, y) ∈ m'
h : {y_1 | ((x, y).fst, y_1) ∈ m ○ n} ⊆ c i
⊢ (x, y).snd ∈ u n
[PROOFSTEP]
refine' ⟨i, m', hm', fun z hz => h (monotone_id.compRel monotone_const mm' _)⟩
[GOAL]
case intro.intro.intro.intro.intro.mk
α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι✝ : Sort u_1
α : Type u
inst✝ : UniformSpace α
s : Set α
ι : Sort u_2
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : s ⊆ ⋃ (i : ι), c i
u : Set (α × α) → Set α := fun n => {x | ∃ i m, m ∈ 𝓤 α ∧ {y | (x, y) ∈ m ○ n} ⊆ c i}
n : Set (α × α)
x✝ : n ∈ 𝓤 α
i : ι
m : Set (α × α)
hm : m ∈ 𝓤 α
m' : Set (α × α)
hm' : m' ∈ 𝓤 α
mm' : m' ○ m' ⊆ m
x y : α
hp : (x, y) ∈ m'
h : {y_1 | ((x, y).fst, y_1) ∈ m ○ n} ⊆ c i
z : α
hz : z ∈ {y_1 | ((x, y).snd, y_1) ∈ m' ○ n}
⊢ ((x, y).fst, z) ∈ (fun x => id x ○ n) (m' ○ m')
[PROOFSTEP]
dsimp [-mem_compRel] at hz ⊢
[GOAL]
case intro.intro.intro.intro.intro.mk
α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι✝ : Sort u_1
α : Type u
inst✝ : UniformSpace α
s : Set α
ι : Sort u_2
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : s ⊆ ⋃ (i : ι), c i
u : Set (α × α) → Set α := fun n => {x | ∃ i m, m ∈ 𝓤 α ∧ {y | (x, y) ∈ m ○ n} ⊆ c i}
n : Set (α × α)
x✝ : n ∈ 𝓤 α
i : ι
m : Set (α × α)
hm : m ∈ 𝓤 α
m' : Set (α × α)
hm' : m' ∈ 𝓤 α
mm' : m' ○ m' ⊆ m
x y : α
hp : (x, y) ∈ m'
h : {y_1 | ((x, y).fst, y_1) ∈ m ○ n} ⊆ c i
z : α
hz : (y, z) ∈ m' ○ n
⊢ (x, z) ∈ m' ○ m' ○ n
[PROOFSTEP]
rw [compRel_assoc]
[GOAL]
case intro.intro.intro.intro.intro.mk
α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι✝ : Sort u_1
α : Type u
inst✝ : UniformSpace α
s : Set α
ι : Sort u_2
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : s ⊆ ⋃ (i : ι), c i
u : Set (α × α) → Set α := fun n => {x | ∃ i m, m ∈ 𝓤 α ∧ {y | (x, y) ∈ m ○ n} ⊆ c i}
n : Set (α × α)
x✝ : n ∈ 𝓤 α
i : ι
m : Set (α × α)
hm : m ∈ 𝓤 α
m' : Set (α × α)
hm' : m' ∈ 𝓤 α
mm' : m' ○ m' ⊆ m
x y : α
hp : (x, y) ∈ m'
h : {y_1 | ((x, y).fst, y_1) ∈ m ○ n} ⊆ c i
z : α
hz : (y, z) ∈ m' ○ n
⊢ (x, z) ∈ m' ○ (m' ○ n)
[PROOFSTEP]
exact ⟨y, hp, hz⟩
[GOAL]
α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι✝ : Sort u_1
α : Type u
inst✝ : UniformSpace α
s : Set α
ι : Sort u_2
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : s ⊆ ⋃ (i : ι), c i
u : Set (α × α) → Set α := fun n => {x | ∃ i m, m ∈ 𝓤 α ∧ {y | (x, y) ∈ m ○ n} ⊆ c i}
hu₁ : ∀ (n : Set (α × α)), n ∈ 𝓤 α → IsOpen (u n)
⊢ ∃ n, n ∈ 𝓤 α ∧ ∀ (x : α), x ∈ s → ∃ i, {y | (x, y) ∈ n} ⊆ c i
[PROOFSTEP]
have hu₂ : s ⊆ ⋃ n ∈ 𝓤 α, u n := fun x hx =>
  by
  rcases mem_iUnion.1 (hc₂ hx) with ⟨i, h⟩
  rcases comp_mem_uniformity_sets (isOpen_uniformity.1 (hc₁ i) x h) with ⟨m', hm', mm'⟩
  exact mem_biUnion hm' ⟨i, _, hm', fun y hy => mm' hy rfl⟩
[GOAL]
α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι✝ : Sort u_1
α : Type u
inst✝ : UniformSpace α
s : Set α
ι : Sort u_2
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : s ⊆ ⋃ (i : ι), c i
u : Set (α × α) → Set α := fun n => {x | ∃ i m, m ∈ 𝓤 α ∧ {y | (x, y) ∈ m ○ n} ⊆ c i}
hu₁ : ∀ (n : Set (α × α)), n ∈ 𝓤 α → IsOpen (u n)
x : α
hx : x ∈ s
⊢ x ∈ ⋃ (n : Set (α × α)) (_ : n ∈ 𝓤 α), u n
[PROOFSTEP]
rcases mem_iUnion.1 (hc₂ hx) with ⟨i, h⟩
[GOAL]
case intro
α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι✝ : Sort u_1
α : Type u
inst✝ : UniformSpace α
s : Set α
ι : Sort u_2
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : s ⊆ ⋃ (i : ι), c i
u : Set (α × α) → Set α := fun n => {x | ∃ i m, m ∈ 𝓤 α ∧ {y | (x, y) ∈ m ○ n} ⊆ c i}
hu₁ : ∀ (n : Set (α × α)), n ∈ 𝓤 α → IsOpen (u n)
x : α
hx : x ∈ s
i : ι
h : x ∈ c i
⊢ x ∈ ⋃ (n : Set (α × α)) (_ : n ∈ 𝓤 α), u n
[PROOFSTEP]
rcases comp_mem_uniformity_sets (isOpen_uniformity.1 (hc₁ i) x h) with ⟨m', hm', mm'⟩
[GOAL]
case intro.intro.intro
α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι✝ : Sort u_1
α : Type u
inst✝ : UniformSpace α
s : Set α
ι : Sort u_2
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : s ⊆ ⋃ (i : ι), c i
u : Set (α × α) → Set α := fun n => {x | ∃ i m, m ∈ 𝓤 α ∧ {y | (x, y) ∈ m ○ n} ⊆ c i}
hu₁ : ∀ (n : Set (α × α)), n ∈ 𝓤 α → IsOpen (u n)
x : α
hx : x ∈ s
i : ι
h : x ∈ c i
m' : Set (α × α)
hm' : m' ∈ 𝓤 α
mm' : m' ○ m' ⊆ {p | p.fst = x → p.snd ∈ c i}
⊢ x ∈ ⋃ (n : Set (α × α)) (_ : n ∈ 𝓤 α), u n
[PROOFSTEP]
exact mem_biUnion hm' ⟨i, _, hm', fun y hy => mm' hy rfl⟩
[GOAL]
α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι✝ : Sort u_1
α : Type u
inst✝ : UniformSpace α
s : Set α
ι : Sort u_2
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : s ⊆ ⋃ (i : ι), c i
u : Set (α × α) → Set α := fun n => {x | ∃ i m, m ∈ 𝓤 α ∧ {y | (x, y) ∈ m ○ n} ⊆ c i}
hu₁ : ∀ (n : Set (α × α)), n ∈ 𝓤 α → IsOpen (u n)
hu₂ : s ⊆ ⋃ (n : Set (α × α)) (_ : n ∈ 𝓤 α), u n
⊢ ∃ n, n ∈ 𝓤 α ∧ ∀ (x : α), x ∈ s → ∃ i, {y | (x, y) ∈ n} ⊆ c i
[PROOFSTEP]
rcases hs.elim_finite_subcover_image hu₁ hu₂ with ⟨b, bu, b_fin, b_cover⟩
[GOAL]
case intro.intro.intro
α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι✝ : Sort u_1
α : Type u
inst✝ : UniformSpace α
s : Set α
ι : Sort u_2
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : s ⊆ ⋃ (i : ι), c i
u : Set (α × α) → Set α := fun n => {x | ∃ i m, m ∈ 𝓤 α ∧ {y | (x, y) ∈ m ○ n} ⊆ c i}
hu₁ : ∀ (n : Set (α × α)), n ∈ 𝓤 α → IsOpen (u n)
hu₂ : s ⊆ ⋃ (n : Set (α × α)) (_ : n ∈ 𝓤 α), u n
b : Set (Set (α × α))
bu : b ⊆ (𝓤 α).sets
b_fin : Set.Finite b
b_cover : s ⊆ ⋃ (i : Set (α × α)) (_ : i ∈ b), u i
⊢ ∃ n, n ∈ 𝓤 α ∧ ∀ (x : α), x ∈ s → ∃ i, {y | (x, y) ∈ n} ⊆ c i
[PROOFSTEP]
refine' ⟨_, (biInter_mem b_fin).2 bu, fun x hx => _⟩
[GOAL]
case intro.intro.intro
α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι✝ : Sort u_1
α : Type u
inst✝ : UniformSpace α
s : Set α
ι : Sort u_2
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : s ⊆ ⋃ (i : ι), c i
u : Set (α × α) → Set α := fun n => {x | ∃ i m, m ∈ 𝓤 α ∧ {y | (x, y) ∈ m ○ n} ⊆ c i}
hu₁ : ∀ (n : Set (α × α)), n ∈ 𝓤 α → IsOpen (u n)
hu₂ : s ⊆ ⋃ (n : Set (α × α)) (_ : n ∈ 𝓤 α), u n
b : Set (Set (α × α))
bu : b ⊆ (𝓤 α).sets
b_fin : Set.Finite b
b_cover : s ⊆ ⋃ (i : Set (α × α)) (_ : i ∈ b), u i
x : α
hx : x ∈ s
⊢ ∃ i, {y | (x, y) ∈ ⋂ (i : Set (α × α)) (_ : i ∈ b), i} ⊆ c i
[PROOFSTEP]
rcases mem_iUnion₂.1 (b_cover hx) with ⟨n, bn, i, m, hm, h⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι✝ : Sort u_1
α : Type u
inst✝ : UniformSpace α
s : Set α
ι : Sort u_2
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : s ⊆ ⋃ (i : ι), c i
u : Set (α × α) → Set α := fun n => {x | ∃ i m, m ∈ 𝓤 α ∧ {y | (x, y) ∈ m ○ n} ⊆ c i}
hu₁ : ∀ (n : Set (α × α)), n ∈ 𝓤 α → IsOpen (u n)
hu₂ : s ⊆ ⋃ (n : Set (α × α)) (_ : n ∈ 𝓤 α), u n
b : Set (Set (α × α))
bu : b ⊆ (𝓤 α).sets
b_fin : Set.Finite b
b_cover : s ⊆ ⋃ (i : Set (α × α)) (_ : i ∈ b), u i
x : α
hx : x ∈ s
n : Set (α × α)
bn : n ∈ b
i : ι
m : Set (α × α)
hm : m ∈ 𝓤 α
h : {y | (x, y) ∈ m ○ n} ⊆ c i
⊢ ∃ i, {y | (x, y) ∈ ⋂ (i : Set (α × α)) (_ : i ∈ b), i} ⊆ c i
[PROOFSTEP]
refine' ⟨i, fun y hy => h _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι✝ : Sort u_1
α : Type u
inst✝ : UniformSpace α
s : Set α
ι : Sort u_2
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : s ⊆ ⋃ (i : ι), c i
u : Set (α × α) → Set α := fun n => {x | ∃ i m, m ∈ 𝓤 α ∧ {y | (x, y) ∈ m ○ n} ⊆ c i}
hu₁ : ∀ (n : Set (α × α)), n ∈ 𝓤 α → IsOpen (u n)
hu₂ : s ⊆ ⋃ (n : Set (α × α)) (_ : n ∈ 𝓤 α), u n
b : Set (Set (α × α))
bu : b ⊆ (𝓤 α).sets
b_fin : Set.Finite b
b_cover : s ⊆ ⋃ (i : Set (α × α)) (_ : i ∈ b), u i
x : α
hx : x ∈ s
n : Set (α × α)
bn : n ∈ b
i : ι
m : Set (α × α)
hm : m ∈ 𝓤 α
h : {y | (x, y) ∈ m ○ n} ⊆ c i
y : α
hy : y ∈ {y | (x, y) ∈ ⋂ (i : Set (α × α)) (_ : i ∈ b), i}
⊢ y ∈ {y | (x, y) ∈ m ○ n}
[PROOFSTEP]
exact prod_mk_mem_compRel (refl_mem_uniformity hm) (biInter_subset_of_mem bn hy)
[GOAL]
α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
α : Type u
inst✝ : UniformSpace α
s : Set α
c : Set (Set α)
hs : IsCompact s
hc₁ : ∀ (t : Set α), t ∈ c → IsOpen t
hc₂ : s ⊆ ⋃₀ c
⊢ ∃ n, n ∈ 𝓤 α ∧ ∀ (x : α), x ∈ s → ∃ t, t ∈ c ∧ ∀ (y : α), (x, y) ∈ n → y ∈ t
[PROOFSTEP]
rw [sUnion_eq_iUnion] at hc₂ 
[GOAL]
α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
α : Type u
inst✝ : UniformSpace α
s : Set α
c : Set (Set α)
hs : IsCompact s
hc₁ : ∀ (t : Set α), t ∈ c → IsOpen t
hc₂ : s ⊆ ⋃ (i : ↑c), ↑i
⊢ ∃ n, n ∈ 𝓤 α ∧ ∀ (x : α), x ∈ s → ∃ t, t ∈ c ∧ ∀ (y : α), (x, y) ∈ n → y ∈ t
[PROOFSTEP]
simpa using lebesgue_number_lemma hs (by simpa) hc₂
[GOAL]
α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
α : Type u
inst✝ : UniformSpace α
s : Set α
c : Set (Set α)
hs : IsCompact s
hc₁ : ∀ (t : Set α), t ∈ c → IsOpen t
hc₂ : s ⊆ ⋃ (i : ↑c), ↑i
⊢ ∀ (i : ↑c), IsOpen ↑i
[PROOFSTEP]
simpa
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
K U : Set α
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
⊢ ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ ∀ (x : α), x ∈ K → UniformSpace.ball x V ⊆ U
[PROOFSTEP]
let W : K → Set (α × α) := fun k => Classical.choose <| isOpen_iff_open_ball_subset.mp hU k.1 <| hKU k.2
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
K U : Set α
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
W : ↑K → Set (α × α) := fun k => Classical.choose (_ : ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ UniformSpace.ball (↑k) V ⊆ U)
⊢ ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ ∀ (x : α), x ∈ K → UniformSpace.ball x V ⊆ U
[PROOFSTEP]
have hW : ∀ k, W k ∈ 𝓤 α ∧ IsOpen (W k) ∧ UniformSpace.ball k.1 (W k) ⊆ U :=
  by
  intro k
  obtain ⟨h₁, h₂, h₃⟩ := Classical.choose_spec (isOpen_iff_open_ball_subset.mp hU k.1 (hKU k.2))
  exact ⟨h₁, h₂, h₃⟩
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
K U : Set α
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
W : ↑K → Set (α × α) := fun k => Classical.choose (_ : ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ UniformSpace.ball (↑k) V ⊆ U)
⊢ ∀ (k : ↑K), W k ∈ 𝓤 α ∧ IsOpen (W k) ∧ UniformSpace.ball (↑k) (W k) ⊆ U
[PROOFSTEP]
intro k
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
K U : Set α
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
W : ↑K → Set (α × α) := fun k => Classical.choose (_ : ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ UniformSpace.ball (↑k) V ⊆ U)
k : ↑K
⊢ W k ∈ 𝓤 α ∧ IsOpen (W k) ∧ UniformSpace.ball (↑k) (W k) ⊆ U
[PROOFSTEP]
obtain ⟨h₁, h₂, h₃⟩ := Classical.choose_spec (isOpen_iff_open_ball_subset.mp hU k.1 (hKU k.2))
[GOAL]
case intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
K U : Set α
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
W : ↑K → Set (α × α) := fun k => Classical.choose (_ : ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ UniformSpace.ball (↑k) V ⊆ U)
k : ↑K
h₁ : Classical.choose (_ : ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ UniformSpace.ball (↑k) V ⊆ U) ∈ 𝓤 α
h₂ : IsOpen (Classical.choose (_ : ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ UniformSpace.ball (↑k) V ⊆ U))
h₃ : UniformSpace.ball (↑k) (Classical.choose (_ : ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ UniformSpace.ball (↑k) V ⊆ U)) ⊆ U
⊢ W k ∈ 𝓤 α ∧ IsOpen (W k) ∧ UniformSpace.ball (↑k) (W k) ⊆ U
[PROOFSTEP]
exact ⟨h₁, h₂, h₃⟩
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
K U : Set α
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
W : ↑K → Set (α × α) := fun k => Classical.choose (_ : ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ UniformSpace.ball (↑k) V ⊆ U)
hW : ∀ (k : ↑K), W k ∈ 𝓤 α ∧ IsOpen (W k) ∧ UniformSpace.ball (↑k) (W k) ⊆ U
⊢ ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ ∀ (x : α), x ∈ K → UniformSpace.ball x V ⊆ U
[PROOFSTEP]
let c : K → Set α := fun k => UniformSpace.ball k.1 (W k)
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
K U : Set α
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
W : ↑K → Set (α × α) := fun k => Classical.choose (_ : ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ UniformSpace.ball (↑k) V ⊆ U)
hW : ∀ (k : ↑K), W k ∈ 𝓤 α ∧ IsOpen (W k) ∧ UniformSpace.ball (↑k) (W k) ⊆ U
c : ↑K → Set α := fun k => UniformSpace.ball (↑k) (W k)
⊢ ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ ∀ (x : α), x ∈ K → UniformSpace.ball x V ⊆ U
[PROOFSTEP]
have hc₁ : ∀ k, IsOpen (c k) := fun k => UniformSpace.isOpen_ball k.1 (hW k).2.1
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
K U : Set α
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
W : ↑K → Set (α × α) := fun k => Classical.choose (_ : ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ UniformSpace.ball (↑k) V ⊆ U)
hW : ∀ (k : ↑K), W k ∈ 𝓤 α ∧ IsOpen (W k) ∧ UniformSpace.ball (↑k) (W k) ⊆ U
c : ↑K → Set α := fun k => UniformSpace.ball (↑k) (W k)
hc₁ : ∀ (k : ↑K), IsOpen (c k)
⊢ ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ ∀ (x : α), x ∈ K → UniformSpace.ball x V ⊆ U
[PROOFSTEP]
have hc₂ : K ⊆ ⋃ i, c i := by
  intro k hk
  simp only [mem_iUnion, SetCoe.exists]
  exact ⟨k, hk, UniformSpace.mem_ball_self k (hW ⟨k, hk⟩).1⟩
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
K U : Set α
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
W : ↑K → Set (α × α) := fun k => Classical.choose (_ : ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ UniformSpace.ball (↑k) V ⊆ U)
hW : ∀ (k : ↑K), W k ∈ 𝓤 α ∧ IsOpen (W k) ∧ UniformSpace.ball (↑k) (W k) ⊆ U
c : ↑K → Set α := fun k => UniformSpace.ball (↑k) (W k)
hc₁ : ∀ (k : ↑K), IsOpen (c k)
⊢ K ⊆ ⋃ (i : ↑K), c i
[PROOFSTEP]
intro k hk
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
K U : Set α
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
W : ↑K → Set (α × α) := fun k => Classical.choose (_ : ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ UniformSpace.ball (↑k) V ⊆ U)
hW : ∀ (k : ↑K), W k ∈ 𝓤 α ∧ IsOpen (W k) ∧ UniformSpace.ball (↑k) (W k) ⊆ U
c : ↑K → Set α := fun k => UniformSpace.ball (↑k) (W k)
hc₁ : ∀ (k : ↑K), IsOpen (c k)
k : α
hk : k ∈ K
⊢ k ∈ ⋃ (i : ↑K), c i
[PROOFSTEP]
simp only [mem_iUnion, SetCoe.exists]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
K U : Set α
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
W : ↑K → Set (α × α) := fun k => Classical.choose (_ : ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ UniformSpace.ball (↑k) V ⊆ U)
hW : ∀ (k : ↑K), W k ∈ 𝓤 α ∧ IsOpen (W k) ∧ UniformSpace.ball (↑k) (W k) ⊆ U
c : ↑K → Set α := fun k => UniformSpace.ball (↑k) (W k)
hc₁ : ∀ (k : ↑K), IsOpen (c k)
k : α
hk : k ∈ K
⊢ ∃ x h,
    k ∈
      UniformSpace.ball x
        (Classical.choose
          (_ : ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ UniformSpace.ball (↑{ val := x, property := (_ : x ∈ K) }) V ⊆ U))
[PROOFSTEP]
exact ⟨k, hk, UniformSpace.mem_ball_self k (hW ⟨k, hk⟩).1⟩
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
K U : Set α
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
W : ↑K → Set (α × α) := fun k => Classical.choose (_ : ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ UniformSpace.ball (↑k) V ⊆ U)
hW : ∀ (k : ↑K), W k ∈ 𝓤 α ∧ IsOpen (W k) ∧ UniformSpace.ball (↑k) (W k) ⊆ U
c : ↑K → Set α := fun k => UniformSpace.ball (↑k) (W k)
hc₁ : ∀ (k : ↑K), IsOpen (c k)
hc₂ : K ⊆ ⋃ (i : ↑K), c i
⊢ ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ ∀ (x : α), x ∈ K → UniformSpace.ball x V ⊆ U
[PROOFSTEP]
have hc₃ : ∀ k, c k ⊆ U := fun k => (hW k).2.2
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
K U : Set α
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
W : ↑K → Set (α × α) := fun k => Classical.choose (_ : ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ UniformSpace.ball (↑k) V ⊆ U)
hW : ∀ (k : ↑K), W k ∈ 𝓤 α ∧ IsOpen (W k) ∧ UniformSpace.ball (↑k) (W k) ⊆ U
c : ↑K → Set α := fun k => UniformSpace.ball (↑k) (W k)
hc₁ : ∀ (k : ↑K), IsOpen (c k)
hc₂ : K ⊆ ⋃ (i : ↑K), c i
hc₃ : ∀ (k : ↑K), c k ⊆ U
⊢ ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ ∀ (x : α), x ∈ K → UniformSpace.ball x V ⊆ U
[PROOFSTEP]
obtain ⟨V, hV, hV'⟩ := lebesgue_number_lemma hK hc₁ hc₂
[GOAL]
case intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
K U : Set α
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
W : ↑K → Set (α × α) := fun k => Classical.choose (_ : ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ UniformSpace.ball (↑k) V ⊆ U)
hW : ∀ (k : ↑K), W k ∈ 𝓤 α ∧ IsOpen (W k) ∧ UniformSpace.ball (↑k) (W k) ⊆ U
c : ↑K → Set α := fun k => UniformSpace.ball (↑k) (W k)
hc₁ : ∀ (k : ↑K), IsOpen (c k)
hc₂ : K ⊆ ⋃ (i : ↑K), c i
hc₃ : ∀ (k : ↑K), c k ⊆ U
V : Set (α × α)
hV : V ∈ 𝓤 α
hV' : ∀ (x : α), x ∈ K → ∃ i, {y | (x, y) ∈ V} ⊆ c i
⊢ ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ ∀ (x : α), x ∈ K → UniformSpace.ball x V ⊆ U
[PROOFSTEP]
refine' ⟨interior V, interior_mem_uniformity hV, isOpen_interior, _⟩
[GOAL]
case intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
K U : Set α
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
W : ↑K → Set (α × α) := fun k => Classical.choose (_ : ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ UniformSpace.ball (↑k) V ⊆ U)
hW : ∀ (k : ↑K), W k ∈ 𝓤 α ∧ IsOpen (W k) ∧ UniformSpace.ball (↑k) (W k) ⊆ U
c : ↑K → Set α := fun k => UniformSpace.ball (↑k) (W k)
hc₁ : ∀ (k : ↑K), IsOpen (c k)
hc₂ : K ⊆ ⋃ (i : ↑K), c i
hc₃ : ∀ (k : ↑K), c k ⊆ U
V : Set (α × α)
hV : V ∈ 𝓤 α
hV' : ∀ (x : α), x ∈ K → ∃ i, {y | (x, y) ∈ V} ⊆ c i
⊢ ∀ (x : α), x ∈ K → UniformSpace.ball x (interior V) ⊆ U
[PROOFSTEP]
intro k hk
[GOAL]
case intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
K U : Set α
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
W : ↑K → Set (α × α) := fun k => Classical.choose (_ : ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ UniformSpace.ball (↑k) V ⊆ U)
hW : ∀ (k : ↑K), W k ∈ 𝓤 α ∧ IsOpen (W k) ∧ UniformSpace.ball (↑k) (W k) ⊆ U
c : ↑K → Set α := fun k => UniformSpace.ball (↑k) (W k)
hc₁ : ∀ (k : ↑K), IsOpen (c k)
hc₂ : K ⊆ ⋃ (i : ↑K), c i
hc₃ : ∀ (k : ↑K), c k ⊆ U
V : Set (α × α)
hV : V ∈ 𝓤 α
hV' : ∀ (x : α), x ∈ K → ∃ i, {y | (x, y) ∈ V} ⊆ c i
k : α
hk : k ∈ K
⊢ UniformSpace.ball k (interior V) ⊆ U
[PROOFSTEP]
obtain ⟨k', hk'⟩ := hV' k hk
[GOAL]
case intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
K U : Set α
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
W : ↑K → Set (α × α) := fun k => Classical.choose (_ : ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ UniformSpace.ball (↑k) V ⊆ U)
hW : ∀ (k : ↑K), W k ∈ 𝓤 α ∧ IsOpen (W k) ∧ UniformSpace.ball (↑k) (W k) ⊆ U
c : ↑K → Set α := fun k => UniformSpace.ball (↑k) (W k)
hc₁ : ∀ (k : ↑K), IsOpen (c k)
hc₂ : K ⊆ ⋃ (i : ↑K), c i
hc₃ : ∀ (k : ↑K), c k ⊆ U
V : Set (α × α)
hV : V ∈ 𝓤 α
hV' : ∀ (x : α), x ∈ K → ∃ i, {y | (x, y) ∈ V} ⊆ c i
k : α
hk : k ∈ K
k' : ↑K
hk' : {y | (k, y) ∈ V} ⊆ c k'
⊢ UniformSpace.ball k (interior V) ⊆ U
[PROOFSTEP]
exact ((ball_mono interior_subset k).trans hk').trans (hc₃ k')
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
f : Filter β
u : β → α
a : α
⊢ Tendsto u f (𝓝 a) ↔ Tendsto (fun x => (a, u x)) f (𝓤 α)
[PROOFSTEP]
rw [nhds_eq_comap_uniformity, tendsto_comap_iff]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
f : Filter β
u : β → α
a : α
⊢ Tendsto (Prod.mk a ∘ u) f (𝓤 α) ↔ Tendsto (fun x => (a, u x)) f (𝓤 α)
[PROOFSTEP]
rfl
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
f : Filter β
u : β → α
a : α
⊢ Tendsto u f (𝓝 a) ↔ Tendsto (fun x => (u x, a)) f (𝓤 α)
[PROOFSTEP]
rw [nhds_eq_comap_uniformity', tendsto_comap_iff]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
f : Filter β
u : β → α
a : α
⊢ Tendsto ((fun y => (y, a)) ∘ u) f (𝓤 α) ↔ Tendsto (fun x => (u x, a)) f (𝓤 α)
[PROOFSTEP]
rfl
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
⊢ ContinuousAt f b ↔ Tendsto (fun x => (f b, f x)) (𝓝 b) (𝓤 α)
[PROOFSTEP]
rw [ContinuousAt, tendsto_nhds_right]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
⊢ ContinuousAt f b ↔ Tendsto (fun x => (f x, f b)) (𝓝 b) (𝓤 α)
[PROOFSTEP]
rw [ContinuousAt, tendsto_nhds_left]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
s : Set β
⊢ ContinuousWithinAt f s b ↔ Tendsto (fun x => (f b, f x)) (𝓝[s] b) (𝓤 α)
[PROOFSTEP]
rw [ContinuousWithinAt, tendsto_nhds_right]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
s : Set β
⊢ ContinuousWithinAt f s b ↔ Tendsto (fun x => (f x, f b)) (𝓝[s] b) (𝓤 α)
[PROOFSTEP]
rw [ContinuousWithinAt, tendsto_nhds_left]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
f : β → α
s : Set β
⊢ ContinuousOn f s ↔ ∀ (b : β), b ∈ s → Tendsto (fun x => (f b, f x)) (𝓝[s] b) (𝓤 α)
[PROOFSTEP]
simp [ContinuousOn, continuousWithinAt_iff'_right]
[GOAL]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
f : β → α
s : Set β
⊢ ContinuousOn f s ↔ ∀ (b : β), b ∈ s → Tendsto (fun x => (f x, f b)) (𝓝[s] b) (𝓤 α)
[PROOFSTEP]
simp [ContinuousOn, continuousWithinAt_iff'_left]
