α : Type u
β : Type v
inst✝ : UniformSpace α
f : Filter α
x : α
adhs : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ t, t ∈ f ∧ t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t
s : Set α
hs : s ∈ 𝓝 x
⊢ s ∈ f
α : Type u
β : Type v
inst✝ : UniformSpace α
f : Filter α
x : α
adhs : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ t, t ∈ f ∧ t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t
⊢ f ≤ 𝓝 x
intro s hs
case intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
f : Filter α
x : α
adhs : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ t, t ∈ f ∧ t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t
s : Set α
hs : s ∈ 𝓝 x
U : Set (α × α)
U_mem : U ∈ 𝓤 α
hU : U ○ U ⊆ {p | p.fst = x → p.snd ∈ s}
⊢ s ∈ f
α : Type u
β : Type v
inst✝ : UniformSpace α
f : Filter α
x : α
adhs : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ t, t ∈ f ∧ t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t
s : Set α
hs : s ∈ 𝓝 x
⊢ s ∈ f
rcases comp_mem_uniformity_sets (mem_nhds_uniformity_iff_right.1 hs) with ⟨U, U_mem, hU⟩
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
f : Filter α
x : α
adhs : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ t, t ∈ f ∧ t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t
s : Set α
hs : s ∈ 𝓝 x
U : Set (α × α)
U_mem : U ∈ 𝓤 α
hU : U ○ U ⊆ {p | p.fst = x → p.snd ∈ s}
t : Set α
t_mem : t ∈ f
ht : t ×ˢ t ⊆ U
y : α
hxy : (x, y) ∈ U
hy : y ∈ t
⊢ s ∈ f
case intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
f : Filter α
x : α
adhs : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ t, t ∈ f ∧ t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t
s : Set α
hs : s ∈ 𝓝 x
U : Set (α × α)
U_mem : U ∈ 𝓤 α
hU : U ○ U ⊆ {p | p.fst = x → p.snd ∈ s}
⊢ s ∈ f
rcases adhs U U_mem with ⟨t, t_mem, ht, y, hxy, hy⟩
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
f : Filter α
x : α
adhs : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ t, t ∈ f ∧ t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t
s : Set α
hs : s ∈ 𝓝 x
U : Set (α × α)
U_mem : U ∈ 𝓤 α
hU : U ○ U ⊆ {p | p.fst = x → p.snd ∈ s}
t : Set α
t_mem : t ∈ f
ht : t ×ˢ t ⊆ U
y : α
hxy : (x, y) ∈ U
hy : y ∈ t
⊢ t ⊆ s
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
f : Filter α
x : α
adhs : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ t, t ∈ f ∧ t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t
s : Set α
hs : s ∈ 𝓝 x
U : Set (α × α)
U_mem : U ∈ 𝓤 α
hU : U ○ U ⊆ {p | p.fst = x → p.snd ∈ s}
t : Set α
t_mem : t ∈ f
ht : t ×ˢ t ⊆ U
y : α
hxy : (x, y) ∈ U
hy : y ∈ t
⊢ s ∈ f
apply mem_of_superset t_mem
no goals
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
f : Filter α
x : α
adhs : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ t, t ∈ f ∧ t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t
s : Set α
hs : s ∈ 𝓝 x
U : Set (α × α)
U_mem : U ∈ 𝓤 α
hU : U ○ U ⊆ {p | p.fst = x → p.snd ∈ s}
t : Set α
t_mem : t ∈ f
ht : t ×ˢ t ⊆ U
y : α
hxy : (x, y) ∈ U
hy : y ∈ t
⊢ t ⊆ s
exact fun z hz => hU (prod_mk_mem_compRel hxy (ht <| mk_mem_prod hy hz)) rfl