α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.27706
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₂
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.27706
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₂
obtain rfl : u₁ = u₂ := UniformSpace.core_eq h
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.27706
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₂
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.27706
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₂
obtain rfl : t₁ = t₂ := topologicalSpace_eq <| funext fun s => by rw [o₁, o₂]
no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.27706
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₂
rfl
no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.27706
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
rw [o₁, o₂]