case left
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.179763
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : ∀ (x : α ⊕ β), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
⊢ s ∈
    (↑OrderDual.toDual ∘ (fun t => ↑OrderDual.toDual {s | IsOpen s}) ∘ ↑OrderDual.ofDual)
      (TopologicalSpace.coinduced inl UniformSpace.toTopologicalSpace)

case right
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.179763
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : ∀ (x : α ⊕ β), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
⊢ s ∈
    (↑OrderDual.toDual ∘ (fun t => ↑OrderDual.toDual {s | IsOpen s}) ∘ ↑OrderDual.ofDual)
      (TopologicalSpace.coinduced inr UniformSpace.toTopologicalSpace)
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.179763
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : ∀ (x : α ⊕ β), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
⊢ IsOpen s
constructor
case left
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.179763
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : ∀ (x : α ⊕ β), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
a : α
ha : a ∈ inl ⁻¹' s
⊢ {p | p.fst = a → p.snd ∈ inl ⁻¹' s} ∈ 𝓤 α
case left
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.179763
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : ∀ (x : α ⊕ β), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
⊢ s ∈
    (↑OrderDual.toDual ∘ (fun t => ↑OrderDual.toDual {s | IsOpen s}) ∘ ↑OrderDual.ofDual)
      (TopologicalSpace.coinduced inl UniformSpace.toTopologicalSpace)
refine' (@isOpen_iff_mem_nhds α _ _).2 fun a ha => mem_nhds_uniformity_iff_right.2 _
case left.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.179763
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : ∀ (x : α ⊕ β), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
a : α
ha : a ∈ inl ⁻¹' s
t : Set (α × α)
ht : t ∈ 𝓤 α
st : (fun p => (inl p.fst, inl p.snd)) '' t ⊆ {p | p.fst = inl a → p.snd ∈ s}
⊢ {p | p.fst = a → p.snd ∈ inl ⁻¹' s} ∈ 𝓤 α
case left
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.179763
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : ∀ (x : α ⊕ β), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
a : α
ha : a ∈ inl ⁻¹' s
⊢ {p | p.fst = a → p.snd ∈ inl ⁻¹' s} ∈ 𝓤 α
rcases mem_map_iff_exists_image.1 (hs _ ha).1 with ⟨t, ht, st⟩
case left.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.179763
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : ∀ (x : α ⊕ β), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
a : α
ha : a ∈ inl ⁻¹' s
t : Set (α × α)
ht : t ∈ 𝓤 α
st : (fun p => (inl p.fst, inl p.snd)) '' t ⊆ {p | p.fst = inl a → p.snd ∈ s}
⊢ t ⊆ {p | p.fst = a → p.snd ∈ inl ⁻¹' s}
case left.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.179763
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : ∀ (x : α ⊕ β), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
a : α
ha : a ∈ inl ⁻¹' s
t : Set (α × α)
ht : t ∈ 𝓤 α
st : (fun p => (inl p.fst, inl p.snd)) '' t ⊆ {p | p.fst = inl a → p.snd ∈ s}
⊢ {p | p.fst = a → p.snd ∈ inl ⁻¹' s} ∈ 𝓤 α
refine' mem_of_superset ht _
case left.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.179763
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : ∀ (x : α ⊕ β), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
t : Set (α × α)
ht : t ∈ 𝓤 α
p : α × α
pt : p ∈ t
ha : p.fst ∈ inl ⁻¹' s
st : (fun p => (inl p.fst, inl p.snd)) '' t ⊆ {p_1 | p_1.fst = inl p.fst → p_1.snd ∈ s}
⊢ p.snd ∈ inl ⁻¹' s
case left.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.179763
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : ∀ (x : α ⊕ β), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
a : α
ha : a ∈ inl ⁻¹' s
t : Set (α × α)
ht : t ∈ 𝓤 α
st : (fun p => (inl p.fst, inl p.snd)) '' t ⊆ {p | p.fst = inl a → p.snd ∈ s}
⊢ t ⊆ {p | p.fst = a → p.snd ∈ inl ⁻¹' s}
rintro p pt rfl
no goals
case left.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.179763
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : ∀ (x : α ⊕ β), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
t : Set (α × α)
ht : t ∈ 𝓤 α
p : α × α
pt : p ∈ t
ha : p.fst ∈ inl ⁻¹' s
st : (fun p => (inl p.fst, inl p.snd)) '' t ⊆ {p_1 | p_1.fst = inl p.fst → p_1.snd ∈ s}
⊢ p.snd ∈ inl ⁻¹' s
exact st ⟨_, pt, rfl⟩ rfl
case right
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.179763
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : ∀ (x : α ⊕ β), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
b : β
hb : b ∈ inr ⁻¹' s
⊢ {p | p.fst = b → p.snd ∈ inr ⁻¹' s} ∈ 𝓤 β
case right
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.179763
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : ∀ (x : α ⊕ β), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
⊢ s ∈
    (↑OrderDual.toDual ∘ (fun t => ↑OrderDual.toDual {s | IsOpen s}) ∘ ↑OrderDual.ofDual)
      (TopologicalSpace.coinduced inr UniformSpace.toTopologicalSpace)
refine' (@isOpen_iff_mem_nhds β _ _).2 fun b hb => mem_nhds_uniformity_iff_right.2 _
case right.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.179763
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : ∀ (x : α ⊕ β), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
b : β
hb : b ∈ inr ⁻¹' s
t : Set (β × β)
ht : t ∈ 𝓤 β
st : (fun p => (inr p.fst, inr p.snd)) '' t ⊆ {p | p.fst = inr b → p.snd ∈ s}
⊢ {p | p.fst = b → p.snd ∈ inr ⁻¹' s} ∈ 𝓤 β
case right
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.179763
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : ∀ (x : α ⊕ β), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
b : β
hb : b ∈ inr ⁻¹' s
⊢ {p | p.fst = b → p.snd ∈ inr ⁻¹' s} ∈ 𝓤 β
rcases mem_map_iff_exists_image.1 (hs _ hb).2 with ⟨t, ht, st⟩
case right.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.179763
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : ∀ (x : α ⊕ β), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
b : β
hb : b ∈ inr ⁻¹' s
t : Set (β × β)
ht : t ∈ 𝓤 β
st : (fun p => (inr p.fst, inr p.snd)) '' t ⊆ {p | p.fst = inr b → p.snd ∈ s}
⊢ t ⊆ {p | p.fst = b → p.snd ∈ inr ⁻¹' s}
case right.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.179763
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : ∀ (x : α ⊕ β), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
b : β
hb : b ∈ inr ⁻¹' s
t : Set (β × β)
ht : t ∈ 𝓤 β
st : (fun p => (inr p.fst, inr p.snd)) '' t ⊆ {p | p.fst = inr b → p.snd ∈ s}
⊢ {p | p.fst = b → p.snd ∈ inr ⁻¹' s} ∈ 𝓤 β
refine' mem_of_superset ht _
case right.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.179763
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : ∀ (x : α ⊕ β), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
t : Set (β × β)
ht : t ∈ 𝓤 β
p : β × β
pt : p ∈ t
hb : p.fst ∈ inr ⁻¹' s
st : (fun p => (inr p.fst, inr p.snd)) '' t ⊆ {p_1 | p_1.fst = inr p.fst → p_1.snd ∈ s}
⊢ p.snd ∈ inr ⁻¹' s
case right.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.179763
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : ∀ (x : α ⊕ β), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
b : β
hb : b ∈ inr ⁻¹' s
t : Set (β × β)
ht : t ∈ 𝓤 β
st : (fun p => (inr p.fst, inr p.snd)) '' t ⊆ {p | p.fst = inr b → p.snd ∈ s}
⊢ t ⊆ {p | p.fst = b → p.snd ∈ inr ⁻¹' s}
rintro p pt rfl
no goals
case right.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.179763
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : ∀ (x : α ⊕ β), x ∈ s → {p | p.fst = x → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
t : Set (β × β)
ht : t ∈ 𝓤 β
p : β × β
pt : p ∈ t
hb : p.fst ∈ inr ⁻¹' s
st : (fun p => (inr p.fst, inr p.snd)) '' t ⊆ {p_1 | p_1.fst = inr p.fst → p_1.snd ∈ s}
⊢ p.snd ∈ inr ⁻¹' s
exact st ⟨_, pt, rfl⟩ rfl