case refine'_1
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56643
inst✝ : UniformSpace α
x : α
s : Set α
⊢ s ∈ 𝓝 x → {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α

case refine'_2
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56643
inst✝ : UniformSpace α
x : α
s : Set α
hs : {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
⊢ s ∈ 𝓝 x
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56643
inst✝ : UniformSpace α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
refine' ⟨_, fun hs => _⟩
case refine'_1
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56643
inst✝ : UniformSpace α
x : α
s : Set α
⊢ ∀ (x_1 : Set α),
    x_1 ⊆ s → (∀ (x : α), x ∈ x_1 → {p | p.fst = x → p.snd ∈ x_1} ∈ 𝓤 α) → x ∈ x_1 → {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
case refine'_1
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56643
inst✝ : UniformSpace α
x : α
s : Set α
⊢ s ∈ 𝓝 x → {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
simp only [mem_nhds_iff, isOpen_uniformity, and_imp, exists_imp]
case refine'_1
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56643
inst✝ : UniformSpace α
x : α
s t : Set α
ts : t ⊆ s
ht : ∀ (x : α), x ∈ t → {p | p.fst = x → p.snd ∈ t} ∈ 𝓤 α
xt : x ∈ t
⊢ {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
case refine'_1
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56643
inst✝ : UniformSpace α
x : α
s : Set α
⊢ ∀ (x_1 : Set α),
    x_1 ⊆ s → (∀ (x : α), x ∈ x_1 → {p | p.fst = x → p.snd ∈ x_1} ∈ 𝓤 α) → x ∈ x_1 → {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
intro t ts ht xt
no goals
case refine'_1
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56643
inst✝ : UniformSpace α
x : α
s t : Set α
ts : t ⊆ s
ht : ∀ (x : α), x ∈ t → {p | p.fst = x → p.snd ∈ t} ∈ 𝓤 α
xt : x ∈ t
⊢ {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
filter_upwards [ht x xt]using fun y h eq => ts (h eq)
case refine'_2.refine'_1
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56643
inst✝ : UniformSpace α
x : α
s : Set α
hs : {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
⊢ {x | {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α} ⊆ s

case refine'_2.refine'_2
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56643
inst✝ : UniformSpace α
x : α
s : Set α
hs : {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
⊢ IsOpen {x | {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α}
case refine'_2
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56643
inst✝ : UniformSpace α
x : α
s : Set α
hs : {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
⊢ s ∈ 𝓝 x
refine' mem_nhds_iff.mpr ⟨{ x | { p : α × α | p.1 = x → p.2 ∈ s } ∈ 𝓤 α }, _, _, hs⟩
no goals
case refine'_2.refine'_1
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56643
inst✝ : UniformSpace α
x : α
s : Set α
hs : {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
⊢ {x | {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α} ⊆ s
exact fun y hy => refl_mem_uniformity hy rfl
case refine'_2.refine'_2
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56643
inst✝ : UniformSpace α
x : α
s : Set α
hs : {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
y : α
hy : y ∈ {x | {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α}
⊢ {p | p.fst = y → p.snd ∈ {x | {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α}} ∈ 𝓤 α
case refine'_2.refine'_2
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56643
inst✝ : UniformSpace α
x : α
s : Set α
hs : {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
⊢ IsOpen {x | {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α}
refine' isOpen_uniformity.mpr fun y hy => _
case refine'_2.refine'_2.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56643
inst✝ : UniformSpace α
x : α
s : Set α
hs : {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
y : α
hy : y ∈ {x | {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α}
t : Set (α × α)
ht : t ∈ 𝓤 α
tr : t ○ t ⊆ {p | p.fst = y → p.snd ∈ s}
⊢ {p | p.fst = y → p.snd ∈ {x | {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α}} ∈ 𝓤 α
case refine'_2.refine'_2
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56643
inst✝ : UniformSpace α
x : α
s : Set α
hs : {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
y : α
hy : y ∈ {x | {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α}
⊢ {p | p.fst = y → p.snd ∈ {x | {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α}} ∈ 𝓤 α
rcases comp_mem_uniformity_sets hy with ⟨t, ht, tr⟩
case h
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56643
inst✝ : UniformSpace α
x : α
s : Set α
hs : {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
y : α
hy : y ∈ {x | {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α}
t : Set (α × α)
ht : t ∈ 𝓤 α
tr : t ○ t ⊆ {p | p.fst = y → p.snd ∈ s}
⊢ ∀ (a : α × α), a ∈ t → a.fst = y → {p | p.fst = a.snd → p.snd ∈ s} ∈ 𝓤 α
case refine'_2.refine'_2.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56643
inst✝ : UniformSpace α
x : α
s : Set α
hs : {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
y : α
hy : y ∈ {x | {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α}
t : Set (α × α)
ht : t ∈ 𝓤 α
tr : t ○ t ⊆ {p | p.fst = y → p.snd ∈ s}
⊢ {p | p.fst = y → p.snd ∈ {x | {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α}} ∈ 𝓤 α
filter_upwards [ht]
case h.mk
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56643
inst✝ : UniformSpace α
x : α
s : Set α
hs : {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
t : Set (α × α)
ht : t ∈ 𝓤 α
a b : α
hp' : (a, b) ∈ t
hy : (a, b).fst ∈ {x | {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α}
tr : t ○ t ⊆ {p | p.fst = (a, b).fst → p.snd ∈ s}
⊢ {p | p.fst = (a, b).snd → p.snd ∈ s} ∈ 𝓤 α
case h
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56643
inst✝ : UniformSpace α
x : α
s : Set α
hs : {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
y : α
hy : y ∈ {x | {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α}
t : Set (α × α)
ht : t ∈ 𝓤 α
tr : t ○ t ⊆ {p | p.fst = y → p.snd ∈ s}
⊢ ∀ (a : α × α), a ∈ t → a.fst = y → {p | p.fst = a.snd → p.snd ∈ s} ∈ 𝓤 α
rintro ⟨a, b⟩ hp' rfl
case h
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56643
inst✝ : UniformSpace α
x : α
s : Set α
hs : {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
t : Set (α × α)
ht : t ∈ 𝓤 α
a b : α
hp' : (a, b) ∈ t
hy : (a, b).fst ∈ {x | {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α}
tr : t ○ t ⊆ {p | p.fst = (a, b).fst → p.snd ∈ s}
⊢ ∀ (a : α × α), a ∈ t → a.fst = b → a.snd ∈ s
case h.mk
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56643
inst✝ : UniformSpace α
x : α
s : Set α
hs : {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
t : Set (α × α)
ht : t ∈ 𝓤 α
a b : α
hp' : (a, b) ∈ t
hy : (a, b).fst ∈ {x | {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α}
tr : t ○ t ⊆ {p | p.fst = (a, b).fst → p.snd ∈ s}
⊢ {p | p.fst = (a, b).snd → p.snd ∈ s} ∈ 𝓤 α
filter_upwards [ht]
case h.mk
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56643
inst✝ : UniformSpace α
x : α
s : Set α
hs : {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
t : Set (α × α)
ht : t ∈ 𝓤 α
a a' b' : α
hp'' : (a', b') ∈ t
hp' : (a, (a', b').fst) ∈ t
hy : (a, (a', b').fst).fst ∈ {x | {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α}
tr : t ○ t ⊆ {p | p.fst = (a, (a', b').fst).fst → p.snd ∈ s}
⊢ (a', b').snd ∈ s
case h
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56643
inst✝ : UniformSpace α
x : α
s : Set α
hs : {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
t : Set (α × α)
ht : t ∈ 𝓤 α
a b : α
hp' : (a, b) ∈ t
hy : (a, b).fst ∈ {x | {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α}
tr : t ○ t ⊆ {p | p.fst = (a, b).fst → p.snd ∈ s}
⊢ ∀ (a : α × α), a ∈ t → a.fst = b → a.snd ∈ s
rintro ⟨a', b'⟩ hp'' rfl
no goals
case h.mk
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56643
inst✝ : UniformSpace α
x : α
s : Set α
hs : {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α
t : Set (α × α)
ht : t ∈ 𝓤 α
a a' b' : α
hp'' : (a', b') ∈ t
hp' : (a, (a', b').fst) ∈ t
hy : (a, (a', b').fst).fst ∈ {x | {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α}
tr : t ○ t ⊆ {p | p.fst = (a, (a', b').fst).fst → p.snd ∈ s}
⊢ (a', b').snd ∈ s
exact @tr (a, b') ⟨a', hp', hp''⟩ rfl