case intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
⊢ IsClosed s
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
⊢ IsClosed s
rcases comp_symm_mem_uniformity_sets V₀_in with ⟨V₁, V₁_in, V₁_symm, h_comp⟩
case intro.intro.intro.h
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
⊢ closure s ⊆ s
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
⊢ IsClosed s
apply isClosed_of_closure_subset
case intro.intro.intro.h
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : x ∈ closure s
⊢ x ∈ s
case intro.intro.intro.h
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
⊢ closure s ⊆ s
intro x hx
case intro.intro.intro.h
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → Set.Nonempty (ball x V ∩ s)
⊢ x ∈ s
case intro.intro.intro.h
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : x ∈ closure s
⊢ x ∈ s
rw [mem_closure_iff_ball] at hx
case intro.intro.intro.h.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → Set.Nonempty (ball x V ∩ s)
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
⊢ x ∈ s
case intro.intro.intro.h
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → Set.Nonempty (ball x V ∩ s)
⊢ x ∈ s
rcases hx V₁_in with ⟨y, hy, hy'⟩
case intro.intro.intro.h.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → Set.Nonempty (ball x V ∩ s)
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
⊢ x = y
case intro.intro.intro.h.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → Set.Nonempty (ball x V ∩ s)
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
⊢ x ∈ s
suffices x = y by rwa [this]
case intro.intro.intro.h.intro.intro.h
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → Set.Nonempty (ball x V ∩ s)
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
⊢ ∀ {V : Set (α × α)}, V ∈ 𝓤 α → SymmetricRel V → (x, y) ∈ V
case intro.intro.intro.h.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → Set.Nonempty (ball x V ∩ s)
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
⊢ x = y
apply eq_of_forall_symmetric
case intro.intro.intro.h.intro.intro.h
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → Set.Nonempty (ball x V ∩ s)
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
V : Set (α × α)
V_in : V ∈ 𝓤 α
a✝ : SymmetricRel V
⊢ (x, y) ∈ V
case intro.intro.intro.h.intro.intro.h
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → Set.Nonempty (ball x V ∩ s)
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
⊢ ∀ {V : Set (α × α)}, V ∈ 𝓤 α → SymmetricRel V → (x, y) ∈ V
intro V V_in _
case intro.intro.intro.h.intro.intro.h.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → Set.Nonempty (ball x V ∩ s)
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
V : Set (α × α)
V_in : V ∈ 𝓤 α
a✝ : SymmetricRel V
z : α
hz : z ∈ ball x (V₁ ∩ V)
hz' : z ∈ s
⊢ (x, y) ∈ V
case intro.intro.intro.h.intro.intro.h
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → Set.Nonempty (ball x V ∩ s)
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
V : Set (α × α)
V_in : V ∈ 𝓤 α
a✝ : SymmetricRel V
⊢ (x, y) ∈ V
rcases hx (inter_mem V₁_in V_in) with ⟨z, hz, hz'⟩
case intro.intro.intro.h.intro.intro.h.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → Set.Nonempty (ball x V ∩ s)
V : Set (α × α)
V_in : V ∈ 𝓤 α
a✝ : SymmetricRel V
z : α
hz : z ∈ ball x (V₁ ∩ V)
hz' : z ∈ s
hy : z ∈ ball x V₁
hy' : z ∈ s
⊢ (x, z) ∈ V
case intro.intro.intro.h.intro.intro.h.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → Set.Nonempty (ball x V ∩ s)
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
V : Set (α × α)
V_in : V ∈ 𝓤 α
a✝ : SymmetricRel V
z : α
hz : z ∈ ball x (V₁ ∩ V)
hz' : z ∈ s
⊢ (x, y) ∈ V
obtain rfl : z = y := by
  by_contra hzy
  exact hs hz' hy' hzy (h_comp <| mem_comp_of_mem_ball V₁_symm (ball_inter_left x _ _ hz) hy)
no goals
case intro.intro.intro.h.intro.intro.h.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → Set.Nonempty (ball x V ∩ s)
V : Set (α × α)
V_in : V ∈ 𝓤 α
a✝ : SymmetricRel V
z : α
hz : z ∈ ball x (V₁ ∩ V)
hz' : z ∈ s
hy : z ∈ ball x V₁
hy' : z ∈ s
⊢ (x, z) ∈ V
exact ball_inter_right x _ _ hz
no goals
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → Set.Nonempty (ball x V ∩ s)
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
this : x = y
⊢ x ∈ s
rwa [this]
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → Set.Nonempty (ball x V ∩ s)
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
V : Set (α × α)
V_in : V ∈ 𝓤 α
a✝ : SymmetricRel V
z : α
hz : z ∈ ball x (V₁ ∩ V)
hz' : z ∈ s
hzy : ¬z = y
⊢ False
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → Set.Nonempty (ball x V ∩ s)
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
V : Set (α × α)
V_in : V ∈ 𝓤 α
a✝ : SymmetricRel V
z : α
hz : z ∈ ball x (V₁ ∩ V)
hz' : z ∈ s
⊢ z = y
by_contra hzy
no goals
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → Set.Nonempty (ball x V ∩ s)
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
V : Set (α × α)
V_in : V ∈ 𝓤 α
a✝ : SymmetricRel V
z : α
hz : z ∈ ball x (V₁ ∩ V)
hz' : z ∈ s
hzy : ¬z = y
⊢ False
exact hs hz' hy' hzy (h_comp <| mem_comp_of_mem_ball V₁_symm (ball_inter_left x _ _ hz) hy)