α : Type u
β : Type v
inst✝ : TopologicalSpace α
⊢ ∀ (a b : α), Disjoint (𝓝 a) (𝓝 b) → {p | Disjoint (𝓝 p.fst) (𝓝 p.snd)} ∈ 𝓝 (a, b)
α : Type u
β : Type v
inst✝ : TopologicalSpace α
⊢ IsOpen {p | Disjoint (𝓝 p.fst) (𝓝 p.snd)}
simp only [isOpen_iff_mem_nhds, Prod.forall, mem_setOf_eq]
α : Type u
β : Type v
inst✝ : TopologicalSpace α
x y : α
h : Disjoint (𝓝 x) (𝓝 y)
⊢ {p | Disjoint (𝓝 p.fst) (𝓝 p.snd)} ∈ 𝓝 (x, y)
α : Type u
β : Type v
inst✝ : TopologicalSpace α
⊢ ∀ (a b : α), Disjoint (𝓝 a) (𝓝 b) → {p | Disjoint (𝓝 p.fst) (𝓝 p.snd)} ∈ 𝓝 (a, b)
intro x y h
case intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : TopologicalSpace α
x y : α
h : Disjoint (𝓝 x) (𝓝 y)
U : Set α
hU : x ∈ U ∧ IsOpen U
V : Set α
hV : y ∈ V ∧ IsOpen V
hd : Disjoint U V
⊢ {p | Disjoint (𝓝 p.fst) (𝓝 p.snd)} ∈ 𝓝 (x, y)
α : Type u
β : Type v
inst✝ : TopologicalSpace α
x y : α
h : Disjoint (𝓝 x) (𝓝 y)
⊢ {p | Disjoint (𝓝 p.fst) (𝓝 p.snd)} ∈ 𝓝 (x, y)
obtain ⟨U, hU, V, hV, hd⟩ := ((nhds_basis_opens x).disjoint_iff (nhds_basis_opens y)).mp h
no goals
case intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : TopologicalSpace α
x y : α
h : Disjoint (𝓝 x) (𝓝 y)
U : Set α
hU : x ∈ U ∧ IsOpen U
V : Set α
hV : y ∈ V ∧ IsOpen V
hd : Disjoint U V
⊢ {p | Disjoint (𝓝 p.fst) (𝓝 p.snd)} ∈ 𝓝 (x, y)
exact
  mem_nhds_prod_iff.mpr
    ⟨U, hU.2.mem_nhds hU.1, V, hV.2.mem_nhds hV.1, fun ⟨x', y'⟩ ⟨hx', hy'⟩ =>
      disjoint_of_disjoint_of_mem hd (hU.2.mem_nhds hx') (hV.2.mem_nhds hy')⟩