α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.89348
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.89348
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d
let ⟨s, hs, hs_comp⟩ := comp3_mem_uniformity hd
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.89348
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
t : Set (α × α)
ht : IsOpen t
hst : s ⊆ t
ht_comp : t ⊆ {p | ∃ x y, (p.fst, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.snd) ∈ s}
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.89348
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d
let ⟨t, ht, hst, ht_comp⟩ := nhdset_of_mem_uniformity s hs
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.89348
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
t : Set (α × α)
ht : IsOpen t
hst : s ⊆ t
ht_comp : t ⊆ {p | ∃ x y, (p.fst, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.snd) ∈ s}
this : s ⊆ interior d
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.89348
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
t : Set (α × α)
ht : IsOpen t
hst : s ⊆ t
ht_comp : t ⊆ {p | ∃ x y, (p.fst, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.snd) ∈ s}
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d
have : s ⊆ interior d :=
  calc
    s ⊆ t := hst
    _ ⊆ interior d :=
      ht.subset_interior_iff.mpr fun x (hx : x ∈ t) =>
        let ⟨x, y, h₁, h₂, h₃⟩ := ht_comp hx
        hs_comp ⟨x, h₁, y, h₂, h₃⟩
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.89348
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
t : Set (α × α)
ht : IsOpen t
hst : s ⊆ t
ht_comp : t ⊆ {p | ∃ x y, (p.fst, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.snd) ∈ s}
this✝ : s ⊆ interior d
this : interior d ∈ 𝓤 α
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.89348
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
t : Set (α × α)
ht : IsOpen t
hst : s ⊆ t
ht_comp : t ⊆ {p | ∃ x y, (p.fst, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.snd) ∈ s}
this : s ⊆ interior d
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d
have : interior d ∈ 𝓤 α := by filter_upwards [hs]using this
no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.89348
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
t : Set (α × α)
ht : IsOpen t
hst : s ⊆ t
ht_comp : t ⊆ {p | ∃ x y, (p.fst, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.snd) ∈ s}
this✝ : s ⊆ interior d
this : interior d ∈ 𝓤 α
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d
simp [this]
no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.89348
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
t : Set (α × α)
ht : IsOpen t
hst : s ⊆ t
ht_comp : t ⊆ {p | ∃ x y, (p.fst, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.snd) ∈ s}
this : s ⊆ interior d
⊢ interior d ∈ 𝓤 α
filter_upwards [hs]using this