α : Type u_2
β : Type u_1
γ : Type ?u.102716
ι : Type ?u.102719
s s' : Set α
x : α
p : Filter ι
g✝ : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : T2Space β
h : ⋃₀ 𝔖 = univ
f g : α →ᵤ[𝔖] β
hfg : f ≠ g
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
α : Type u_2
β : Type u_1
γ : Type ?u.102716
ι : Type ?u.102719
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : T2Space β
h : ⋃₀ 𝔖 = univ
⊢ ∀ (x y : α →ᵤ[𝔖] β), x ≠ y → ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
intro f g hfg
case intro
α : Type u_2
β : Type u_1
γ : Type ?u.102716
ι : Type ?u.102719
s s' : Set α
x✝ : α
p : Filter ι
g✝ : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : T2Space β
h : ⋃₀ 𝔖 = univ
f g : α →ᵤ[𝔖] β
hfg : f ≠ g
x : α
hx : ¬f x = g x
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
α : Type u_2
β : Type u_1
γ : Type ?u.102716
ι : Type ?u.102719
s s' : Set α
x : α
p : Filter ι
g✝ : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : T2Space β
h : ⋃₀ 𝔖 = univ
f g : α →ᵤ[𝔖] β
hfg : f ≠ g
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
obtain ⟨x, hx⟩ := not_forall.mp (mt funext hfg)
case intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.102716
ι : Type ?u.102719
s✝ s' : Set α
x✝ : α
p : Filter ι
g✝ : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : T2Space β
h : ⋃₀ 𝔖 = univ
f g : α →ᵤ[𝔖] β
hfg : f ≠ g
x : α
hx : ¬f x = g x
s : Set α
hs : s ∈ 𝔖
hxs : x ∈ s
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
case intro
α : Type u_2
β : Type u_1
γ : Type ?u.102716
ι : Type ?u.102719
s s' : Set α
x✝ : α
p : Filter ι
g✝ : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : T2Space β
h : ⋃₀ 𝔖 = univ
f g : α →ᵤ[𝔖] β
hfg : f ≠ g
x : α
hx : ¬f x = g x
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
obtain ⟨s, hs, hxs⟩ : ∃ s ∈ 𝔖, x ∈ s := mem_sUnion.mp (h.symm ▸ True.intro)
no goals
case intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.102716
ι : Type ?u.102719
s✝ s' : Set α
x✝ : α
p : Filter ι
g✝ : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : T2Space β
h : ⋃₀ 𝔖 = univ
f g : α →ᵤ[𝔖] β
hfg : f ≠ g
x : α
hx : ¬f x = g x
s : Set α
hs : s ∈ 𝔖
hxs : x ∈ s
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
exact separated_by_continuous (uniformContinuous_eval_of_mem β 𝔖 hxs hs).continuous hx