case mp
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
h : SeparatedSpace α
⊢ T2Space α

case mpr
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
h : T2Space α
⊢ SeparatedSpace α
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ SeparatedSpace α ↔ T2Space α
constructor <;> intro h
case mp
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
h : SeparatedSpace α
⊢ IsClosed (𝓢 α)
case mp
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
h : SeparatedSpace α
⊢ T2Space α
rw [t2_iff_isClosed_diagonal, ← show 𝓢 α = diagonal α from h.1]
no goals
case mp
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
h : SeparatedSpace α
⊢ IsClosed (𝓢 α)
exact isClosed_separationRel
case mpr
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
h : T2Space α
⊢ ∀ (x y : α), x ≠ y → ∃ r, r ∈ 𝓤 α ∧ ¬(x, y) ∈ r
case mpr
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
h : T2Space α
⊢ SeparatedSpace α
rw [separated_def']
case mpr
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
h : T2Space α
x y : α
hxy : x ≠ y
⊢ ∃ r, r ∈ 𝓤 α ∧ ¬(x, y) ∈ r
case mpr
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
h : T2Space α
⊢ ∀ (x y : α), x ≠ y → ∃ r, r ∈ 𝓤 α ∧ ¬(x, y) ∈ r
intro x y hxy
case mpr.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
h✝ : T2Space α
x y : α
hxy : x ≠ y
u v : Set α
uo : IsOpen u
hx : x ∈ u
hy : y ∈ v
h : Disjoint u v
⊢ ∃ r, r ∈ 𝓤 α ∧ ¬(x, y) ∈ r
case mpr
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
h : T2Space α
x y : α
hxy : x ≠ y
⊢ ∃ r, r ∈ 𝓤 α ∧ ¬(x, y) ∈ r
rcases t2_separation hxy with ⟨u, v, uo, -, hx, hy, h⟩
case mpr.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
h✝ : T2Space α
x y : α
hxy : x ≠ y
u v : Set α
uo : IsOpen u
hx : x ∈ u
hy : y ∈ v
h : Disjoint u v
r : Set (α × α)
hrU : r ∈ 𝓤 α
hr : ball x r ⊆ u
⊢ ∃ r, r ∈ 𝓤 α ∧ ¬(x, y) ∈ r
case mpr.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
h✝ : T2Space α
x y : α
hxy : x ≠ y
u v : Set α
uo : IsOpen u
hx : x ∈ u
hy : y ∈ v
h : Disjoint u v
⊢ ∃ r, r ∈ 𝓤 α ∧ ¬(x, y) ∈ r
rcases isOpen_iff_ball_subset.1 uo x hx with ⟨r, hrU, hr⟩
no goals
case mpr.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
h✝ : T2Space α
x y : α
hxy : x ≠ y
u v : Set α
uo : IsOpen u
hx : x ∈ u
hy : y ∈ v
h : Disjoint u v
r : Set (α × α)
hrU : r ∈ 𝓤 α
hr : ball x r ⊆ u
⊢ ∃ r, r ∈ 𝓤 α ∧ ¬(x, y) ∈ r
exact ⟨r, hrU, fun H => h.le_bot ⟨hr H, hy⟩⟩