α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.87316
inst✝ : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
⊢ ∃ r, r ∈ 𝓤 α ∧ IsClosed r ∧ r ⊆ t
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.87316
inst✝ : UniformSpace α
⊢ HasBasis (𝓤 α) (fun V => V ∈ 𝓤 α ∧ IsClosed V) id
refine' Filter.hasBasis_self.2 fun t h => _
case intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.87316
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
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.87316
inst✝ : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
⊢ ∃ r, r ∈ 𝓤 α ∧ IsClosed r ∧ r ⊆ t
rcases comp_comp_symm_mem_uniformity_sets h with ⟨w, w_in, w_symm, r⟩
case intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.87316
inst✝ : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
r : w ○ w ○ w ⊆ t
⊢ closure w ⊆ t
case intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.87316
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
refine' ⟨closure w, mem_of_superset w_in subset_closure, isClosed_closure, _⟩
case intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.87316
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
case intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.87316
inst✝ : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
r : w ○ w ○ w ⊆ t
⊢ closure w ⊆ t
refine' Subset.trans _ r
case intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.87316
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
case intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.87316
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
rw [closure_eq_uniformity]
case intro.intro.intro.h
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.87316
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.87316
inst✝ : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
r : w ○ w ○ w ⊆ t
⊢ Set (α × α)
case intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.87316
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
apply iInter_subset_of_subset
case intro.intro.intro.h.i
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.87316
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}
case intro.intro.intro.h
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.87316
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.87316
inst✝ : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
r : w ○ w ○ w ⊆ t
⊢ Set (α × α)
apply iInter_subset
no goals
case intro.intro.intro.h.i
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.87316
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}
exact ⟨w_in, w_symm⟩