Disjoint unions and products of topological spaces

This file constructs sums (disjoint unions) and products of topological spaces and sets up their basic theory, such as criteria for maps into or out of these constructions to be continuous; descriptions of the open sets, neighborhood filters, and generators of these constructions; and their behavior with respect to embeddings and other specific classes of maps.

We also provide basic homeomorphisms, to show that sums and products are commutative, associative and distributive (up to homeomorphism).

Implementation note

The constructed topologies are defined using induced and coinduced topologies along with the complete lattice structure on topologies. Their universal properties (for example, a map X → Y × Z is continuous if and only if both projections X → Y, X → Z are) follow easily using order-theoretic descriptions of continuity. With more work we can also extract descriptions of the open sets, neighborhood filters and so on.

Tags

product, sum, disjoint union

instance instTopologicalSpaceSum {X : Type u} {Y : Type v} [t₁ : TopologicalSpace X] [t₂ : TopologicalSpace Y] : TopologicalSpace (X ⊕ Y)

Equations

• instTopologicalSpaceSum = TopologicalSpace.coinduced Sum.inl t₁ ⊔ TopologicalSpace.coinduced Sum.inr t₂

instance instTopologicalSpaceProd {X : Type u} {Y : Type v} [t₁ : TopologicalSpace X] [t₂ : TopologicalSpace Y] : TopologicalSpace (X × Y)

Equations

• instTopologicalSpaceProd = TopologicalSpace.induced Prod.fst t₁ ⊓ TopologicalSpace.induced Prod.snd t₂

@[simp]

theorem continuous_prod_mk {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y} {g : X → Z} : (Continuous fun (x : X) => (f x, g x)) ↔ Continuous f ∧ Continuous g

theorem continuous_fst {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : Continuous Prod.fst

theorem Continuous.fst {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y × Z} (hf : Continuous f) : Continuous fun (x : X) => (f x).1

Postcomposing f with Prod.fst is continuous

theorem Continuous.fst' {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Z} (hf : Continuous f) : Continuous fun (x : X × Y) => f x.1

Precomposing f with Prod.fst is continuous

theorem continuousAt_fst {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {p : X × Y} : ContinuousAt Prod.fst p

theorem ContinuousAt.fst {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y × Z} {x : X} (hf : ContinuousAt f x) : ContinuousAt (fun (x : X) => (f x).1) x

Postcomposing f with Prod.fst is continuous at x

theorem ContinuousAt.fst' {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Z} {x : X} {y : Y} (hf : ContinuousAt f x) : ContinuousAt (fun (x : X × Y) => f x.1) (x, y)

Precomposing f with Prod.fst is continuous at (x, y)

theorem ContinuousAt.fst'' {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Z} {x : X × Y} (hf : ContinuousAt f x.1) : ContinuousAt (fun (x : X × Y) => f x.1) x

Precomposing f with Prod.fst is continuous at x : X × Y

theorem Filter.Tendsto.fst_nhds {Y : Type v} {Z : Type u_2} [TopologicalSpace Y] [TopologicalSpace Z] {X : Type u_5} {l : Filter X} {f : X → Y × Z} {p : Y × Z} (h : Tendsto f l (nhds p)) : Tendsto (fun (a : X) => (f a).1) l (nhds p.1)

theorem continuous_snd {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : Continuous Prod.snd

theorem Continuous.snd {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y × Z} (hf : Continuous f) : Continuous fun (x : X) => (f x).2

Postcomposing f with Prod.snd is continuous

theorem Continuous.snd' {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : Y → Z} (hf : Continuous f) : Continuous fun (x : X × Y) => f x.2

Precomposing f with Prod.snd is continuous

theorem continuousAt_snd {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {p : X × Y} : ContinuousAt Prod.snd p

theorem ContinuousAt.snd {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y × Z} {x : X} (hf : ContinuousAt f x) : ContinuousAt (fun (x : X) => (f x).2) x

Postcomposing f with Prod.snd is continuous at x

theorem ContinuousAt.snd' {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : Y → Z} {x : X} {y : Y} (hf : ContinuousAt f y) : ContinuousAt (fun (x : X × Y) => f x.2) (x, y)

Precomposing f with Prod.snd is continuous at (x, y)

theorem ContinuousAt.snd'' {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : Y → Z} {x : X × Y} (hf : ContinuousAt f x.2) : ContinuousAt (fun (x : X × Y) => f x.2) x

Precomposing f with Prod.snd is continuous at x : X × Y

theorem Filter.Tendsto.snd_nhds {Y : Type v} {Z : Type u_2} [TopologicalSpace Y] [TopologicalSpace Z] {X : Type u_5} {l : Filter X} {f : X → Y × Z} {p : Y × Z} (h : Tendsto f l (nhds p)) : Tendsto (fun (a : X) => (f a).2) l (nhds p.2)

theorem Continuous.prod_mk {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : Z → X} {g : Z → Y} (hf : Continuous f) (hg : Continuous g) : Continuous fun (x : Z) => (f x, g x)

theorem Continuous.Prod.mk {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (x : X) : Continuous fun (y : Y) => (x, y)

theorem Continuous.Prod.mk_left {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (y : Y) : Continuous fun (x : X) => (x, y)

theorem IsClosed.setOf_mapsTo {X : Type u} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Z] {α : Type u_5} {f : X → α → Z} {s : Set α} {t : Set Z} (ht : IsClosed t) (hf : ∀ a ∈ s, Continuous fun (x : X) => f x a) : IsClosed {x : X | Set.MapsTo (f x) s t}

If f x y is continuous in x for all y ∈ s, then the set of x such that f x maps s to t is closed.

theorem Continuous.comp₂ {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {g : X × Y → Z} (hg : Continuous g) {e : W → X} (he : Continuous e) {f : W → Y} (hf : Continuous f) : Continuous fun (w : W) => g (e w, f w)

theorem Continuous.comp₃ {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} {ε : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] [TopologicalSpace ε] {g : X × Y × Z → ε} (hg : Continuous g) {e : W → X} (he : Continuous e) {f : W → Y} (hf : Continuous f) {k : W → Z} (hk : Continuous k) : Continuous fun (w : W) => g (e w, f w, k w)

theorem Continuous.comp₄ {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} {ε : Type u_3} {ζ : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] [TopologicalSpace ε] [TopologicalSpace ζ] {g : X × Y × Z × ζ → ε} (hg : Continuous g) {e : W → X} (he : Continuous e) {f : W → Y} (hf : Continuous f) {k : W → Z} (hk : Continuous k) {l : W → ζ} (hl : Continuous l) : Continuous fun (w : W) => g (e w, f w, k w, l w)

theorem Continuous.prodMap {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : Z → X} {g : W → Y} (hf : Continuous f) (hg : Continuous g) : Continuous (Prod.map f g)

@[deprecated Continuous.prodMap (since := "2024-10-05")]

theorem Continuous.prod_map {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : Z → X} {g : W → Y} (hf : Continuous f) (hg : Continuous g) : Continuous (Prod.map f g)

Alias of Continuous.prodMap.

theorem continuous_inf_dom_left₂ {X : Type u_5} {Y : Type u_6} {Z : Type u_7} {f : X → Y → Z} {ta1 ta2 : TopologicalSpace X} {tb1 tb2 : TopologicalSpace Y} {tc1 : TopologicalSpace Z} (h : Continuous fun (p : X × Y) => f p.1 p.2) : Continuous fun (p : X × Y) => f p.1 p.2

A version of continuous_inf_dom_left for binary functions

theorem continuous_inf_dom_right₂ {X : Type u_5} {Y : Type u_6} {Z : Type u_7} {f : X → Y → Z} {ta1 ta2 : TopologicalSpace X} {tb1 tb2 : TopologicalSpace Y} {tc1 : TopologicalSpace Z} (h : Continuous fun (p : X × Y) => f p.1 p.2) : Continuous fun (p : X × Y) => f p.1 p.2

A version of continuous_inf_dom_right for binary functions

theorem continuous_sInf_dom₂ {X : Type u_5} {Y : Type u_6} {Z : Type u_7} {f : X → Y → Z} {tas : Set (TopologicalSpace X)} {tbs : Set (TopologicalSpace Y)} {tX : TopologicalSpace X} {tY : TopologicalSpace Y} {tc : TopologicalSpace Z} (hX : tX ∈ tas) (hY : tY ∈ tbs) (hf : Continuous fun (p : X × Y) => f p.1 p.2) : Continuous fun (p : X × Y) => f p.1 p.2

A version of continuous_sInf_dom for binary functions

theorem Filter.Eventually.prod_inl_nhds {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {p : X → Prop} {x : X} (h : ∀ᶠ (x : X) in nhds x, p x) (y : Y) : ∀ᶠ (x : X × Y) in nhds (x, y), p x.1

theorem Filter.Eventually.prod_inr_nhds {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {p : Y → Prop} {y : Y} (h : ∀ᶠ (x : Y) in nhds y, p x) (x : X) : ∀ᶠ (x : X × Y) in nhds (x, y), p x.2

theorem Filter.Eventually.prod_mk_nhds {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {px : X → Prop} {x : X} (hx : ∀ᶠ (x : X) in nhds x, px x) {py : Y → Prop} {y : Y} (hy : ∀ᶠ (y : Y) in nhds y, py y) : ∀ᶠ (p : X × Y) in nhds (x, y), px p.1 ∧ py p.2

theorem continuous_swap {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : Continuous Prod.swap

theorem isClosedMap_swap {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : IsClosedMap Prod.swap

theorem Continuous.uncurry_left {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y → Z} (x : X) (h : Continuous (Function.uncurry f)) : Continuous (f x)

theorem Continuous.uncurry_right {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y → Z} (y : Y) (h : Continuous (Function.uncurry f)) : Continuous fun (a : X) => f a y

theorem continuous_curry {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {g : X × Y → Z} (x : X) (h : Continuous g) : Continuous (Function.curry g x)

theorem IsOpen.prod {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {t : Set Y} (hs : IsOpen s) (ht : IsOpen t) : IsOpen (s ×ˢ t)

theorem nhds_prod_eq {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} : nhds (x, y) = nhds x ×ˢ nhds y

theorem nhdsWithin_prod_eq {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (x : X) (y : Y) (s : Set X) (t : Set Y) : nhdsWithin (x, y) (s ×ˢ t) = nhdsWithin x s ×ˢ nhdsWithin y t

instance Prod.instNeBotNhdsWithinIio {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [Preorder X] [Preorder Y] {x : X × Y} [hx₁ : (nhdsWithin x.1 (Set.Iio x.1)).NeBot] [hx₂ : (nhdsWithin x.2 (Set.Iio x.2)).NeBot] : (nhdsWithin x (Set.Iio x)).NeBot

theorem mem_nhds_prod_iff {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} {s : Set (X × Y)} : s ∈ nhds (x, y) ↔ ∃ u ∈ nhds x, ∃ v ∈ nhds y, u ×ˢ v ⊆ s

theorem mem_nhdsWithin_prod_iff {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} {s : Set (X × Y)} {tx : Set X} {ty : Set Y} : s ∈ nhdsWithin (x, y) (tx ×ˢ ty) ↔ ∃ u ∈ nhdsWithin x tx, ∃ v ∈ nhdsWithin y ty, u ×ˢ v ⊆ s

theorem Filter.HasBasis.prod_nhds {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {ιX : Type u_5} {ιY : Type u_6} {px : ιX → Prop} {py : ιY → Prop} {sx : ιX → Set X} {sy : ιY → Set Y} {x : X} {y : Y} (hx : (nhds x).HasBasis px sx) (hy : (nhds y).HasBasis py sy) : (nhds (x, y)).HasBasis (fun (i : ιX × ιY) => px i.1 ∧ py i.2) fun (i : ιX × ιY) => sx i.1 ×ˢ sy i.2

theorem Filter.HasBasis.prod_nhds' {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {ιX : Type u_5} {ιY : Type u_6} {pX : ιX → Prop} {pY : ιY → Prop} {sx : ιX → Set X} {sy : ιY → Set Y} {p : X × Y} (hx : (nhds p.1).HasBasis pX sx) (hy : (nhds p.2).HasBasis pY sy) : (nhds p).HasBasis (fun (i : ιX × ιY) => pX i.1 ∧ pY i.2) fun (i : ιX × ιY) => sx i.1 ×ˢ sy i.2

theorem mem_nhds_prod_iff' {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} {s : Set (X × Y)} : s ∈ nhds (x, y) ↔ ∃ (u : Set X) (v : Set Y), IsOpen u ∧ x ∈ u ∧ IsOpen v ∧ y ∈ v ∧ u ×ˢ v ⊆ s

theorem Prod.tendsto_iff {Y : Type v} {Z : Type u_2} [TopologicalSpace Y] [TopologicalSpace Z] {X : Type u_5} (seq : X → Y × Z) {f : Filter X} (p : Y × Z) : Filter.Tendsto seq f (nhds p) ↔ Filter.Tendsto (fun (n : X) => (seq n).1) f (nhds p.1) ∧ Filter.Tendsto (fun (n : X) => (seq n).2) f (nhds p.2)

instance instDiscreteTopologyProd {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [DiscreteTopology X] [DiscreteTopology Y] : DiscreteTopology (X × Y)

theorem prod_mem_nhds_iff {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {t : Set Y} {x : X} {y : Y} : s ×ˢ t ∈ nhds (x, y) ↔ s ∈ nhds x ∧ t ∈ nhds y

theorem prod_mem_nhds {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {t : Set Y} {x : X} {y : Y} (hx : s ∈ nhds x) (hy : t ∈ nhds y) : s ×ˢ t ∈ nhds (x, y)

theorem isOpen_setOf_disjoint_nhds_nhds {X : Type u} [TopologicalSpace X] : IsOpen {p : X × X | Disjoint (nhds p.1) (nhds p.2)}

theorem Filter.Eventually.prod_nhds {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {p : X → Prop} {q : Y → Prop} {x : X} {y : Y} (hx : ∀ᶠ (x : X) in nhds x, p x) (hy : ∀ᶠ (y : Y) in nhds y, q y) : ∀ᶠ (z : X × Y) in nhds (x, y), p z.1 ∧ q z.2

theorem Filter.EventuallyEq.prodMap_nhds {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {α : Type u_5} {β : Type u_6} {f₁ f₂ : X → α} {g₁ g₂ : Y → β} {x : X} {y : Y} (hf : f₁ =ᶠ[nhds x] f₂) (hg : g₁ =ᶠ[nhds y] g₂) : Prod.map f₁ g₁ =ᶠ[nhds (x, y)] Prod.map f₂ g₂

theorem Filter.EventuallyLE.prodMap_nhds {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {α : Type u_5} {β : Type u_6} [LE α] [LE β] {f₁ f₂ : X → α} {g₁ g₂ : Y → β} {x : X} {y : Y} (hf : f₁ ≤ᶠ[nhds x] f₂) (hg : g₁ ≤ᶠ[nhds y] g₂) : Prod.map f₁ g₁ ≤ᶠ[nhds (x, y)] Prod.map f₂ g₂

theorem nhds_swap {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (x : X) (y : Y) : nhds (x, y) = Filter.map Prod.swap (nhds (y, x))

theorem Filter.Tendsto.prod_mk_nhds {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {γ : Type u_5} {x : X} {y : Y} {f : Filter γ} {mx : γ → X} {my : γ → Y} (hx : Tendsto mx f (nhds x)) (hy : Tendsto my f (nhds y)) : Tendsto (fun (c : γ) => (mx c, my c)) f (nhds (x, y))

theorem Filter.Tendsto.prodMap_nhds {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {x : X} {y : Y} {z : Z} {w : W} {f : X → Y} {g : Z → W} (hf : Tendsto f (nhds x) (nhds y)) (hg : Tendsto g (nhds z) (nhds w)) : Tendsto (Prod.map f g) (nhds (x, z)) (nhds (y, w))

theorem Filter.Eventually.curry_nhds {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {p : X × Y → Prop} {x : X} {y : Y} (h : ∀ᶠ (x : X × Y) in nhds (x, y), p x) : ∀ᶠ (x' : X) in nhds x, ∀ᶠ (y' : Y) in nhds y, p (x', y')

theorem ContinuousAt.prod {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y} {g : X → Z} {x : X} (hf : ContinuousAt f x) (hg : ContinuousAt g x) : ContinuousAt (fun (x : X) => (f x, g x)) x

theorem ContinuousAt.prodMap {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : X → Z} {g : Y → W} {p : X × Y} (hf : ContinuousAt f p.1) (hg : ContinuousAt g p.2) : ContinuousAt (Prod.map f g) p

@[deprecated ContinuousAt.prodMap (since := "2024-10-05")]

theorem ContinuousAt.prod_map {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : X → Z} {g : Y → W} {p : X × Y} (hf : ContinuousAt f p.1) (hg : ContinuousAt g p.2) : ContinuousAt (Prod.map f g) p

Alias of ContinuousAt.prodMap.

theorem ContinuousAt.prodMap' {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : X → Z} {g : Y → W} {x : X} {y : Y} (hf : ContinuousAt f x) (hg : ContinuousAt g y) : ContinuousAt (Prod.map f g) (x, y)

A version of ContinuousAt.prodMap that avoids Prod.fst/Prod.snd by assuming that the point is (x, y).

@[deprecated ContinuousAt.prodMap' (since := "2024-10-05")]

theorem ContinuousAt.prod_map' {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : X → Z} {g : Y → W} {x : X} {y : Y} (hf : ContinuousAt f x) (hg : ContinuousAt g y) : ContinuousAt (Prod.map f g) (x, y)

Alias of ContinuousAt.prodMap'.

---

A version of ContinuousAt.prodMap that avoids Prod.fst/Prod.snd by assuming that the point is (x, y).

theorem ContinuousAt.comp₂ {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : Y × Z → W} {g : X → Y} {h : X → Z} {x : X} (hf : ContinuousAt f (g x, h x)) (hg : ContinuousAt g x) (hh : ContinuousAt h x) : ContinuousAt (fun (x : X) => f (g x, h x)) x

theorem ContinuousAt.comp₂_of_eq {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : Y × Z → W} {g : X → Y} {h : X → Z} {x : X} {y : Y × Z} (hf : ContinuousAt f y) (hg : ContinuousAt g x) (hh : ContinuousAt h x) (e : (g x, h x) = y) : ContinuousAt (fun (x : X) => f (g x, h x)) x

theorem Continuous.curry_left {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X × Y → Z} (hf : Continuous f) {y : Y} : Continuous fun (x : X) => f (x, y)

Continuous functions on products are continuous in their first argument

theorem Continuous.along_fst {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X × Y → Z} (hf : Continuous f) {y : Y} : Continuous fun (x : X) => f (x, y)

Alias of Continuous.curry_left.

---

Continuous functions on products are continuous in their first argument

theorem Continuous.curry_right {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X × Y → Z} (hf : Continuous f) {x : X} : Continuous fun (y : Y) => f (x, y)

Continuous functions on products are continuous in their second argument

theorem Continuous.along_snd {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X × Y → Z} (hf : Continuous f) {x : X} : Continuous fun (y : Y) => f (x, y)

Alias of Continuous.curry_right.

---

Continuous functions on products are continuous in their second argument

theorem prod_generateFrom_generateFrom_eq {X : Type u_5} {Y : Type u_6} {s : Set (Set X)} {t : Set (Set Y)} (hs : ⋃₀ s = Set.univ) (ht : ⋃₀ t = Set.univ) : instTopologicalSpaceProd = TopologicalSpace.generateFrom (Set.image2 (fun (x1 : Set X) (x2 : Set Y) => x1 ×ˢ x2) s t)

theorem prod_eq_generateFrom {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : instTopologicalSpaceProd = TopologicalSpace.generateFrom {g : Set (X × Y) | ∃ (s : Set X) (t : Set Y), IsOpen s ∧ IsOpen t ∧ g = s ×ˢ t}

theorem isOpen_prod_iff {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set (X × Y)} : IsOpen s ↔ ∀ (a : X) (b : Y), (a, b) ∈ s → ∃ (u : Set X) (v : Set Y), IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ s

theorem prod_induced_induced {Y : Type v} {W : Type u_1} [TopologicalSpace Y] [TopologicalSpace W] {X : Type u_5} {Z : Type u_6} (f : X → Y) (g : Z → W) : instTopologicalSpaceProd = TopologicalSpace.induced (fun (p : X × Z) => (f p.1, g p.2)) instTopologicalSpaceProd

A product of induced topologies is induced by the product map

theorem exists_nhds_square {X : Type u} [TopologicalSpace X] {s : Set (X × X)} {x : X} (hx : s ∈ nhds (x, x)) : ∃ (U : Set X), IsOpen U ∧ x ∈ U ∧ U ×ˢ U ⊆ s

Given a neighborhood s of (x, x), then (x, x) has a square open neighborhood that is a subset of s.

theorem map_fst_nhdsWithin {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (x : X × Y) : Filter.map Prod.fst (nhdsWithin x (Prod.snd ⁻¹' {x.2})) = nhds x.1

Prod.fst maps neighborhood of x : X × Y within the section Prod.snd ⁻¹' {x.2} to 𝓝 x.1.

@[simp]

theorem map_fst_nhds {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (x : X × Y) : Filter.map Prod.fst (nhds x) = nhds x.1

theorem isOpenMap_fst {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : IsOpenMap Prod.fst

The first projection in a product of topological spaces sends open sets to open sets.

theorem map_snd_nhdsWithin {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (x : X × Y) : Filter.map Prod.snd (nhdsWithin x (Prod.fst ⁻¹' {x.1})) = nhds x.2

Prod.snd maps neighborhood of x : X × Y within the section Prod.fst ⁻¹' {x.1} to 𝓝 x.2.

@[simp]

theorem map_snd_nhds {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (x : X × Y) : Filter.map Prod.snd (nhds x) = nhds x.2

theorem isOpenMap_snd {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : IsOpenMap Prod.snd

The second projection in a product of topological spaces sends open sets to open sets.

theorem isOpen_prod_iff' {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {t : Set Y} : IsOpen (s ×ˢ t) ↔ IsOpen s ∧ IsOpen t ∨ s = ∅ ∨ t = ∅

A product set is open in a product space if and only if each factor is open, or one of them is empty

theorem isQuotientMap_fst {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [Nonempty Y] : Topology.IsQuotientMap Prod.fst

@[deprecated isQuotientMap_fst (since := "2024-10-22")]

theorem quotientMap_fst {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [Nonempty Y] : Topology.IsQuotientMap Prod.fst

Alias of isQuotientMap_fst.

theorem isQuotientMap_snd {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [Nonempty X] : Topology.IsQuotientMap Prod.snd

@[deprecated isQuotientMap_snd (since := "2024-10-22")]

theorem quotientMap_snd {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [Nonempty X] : Topology.IsQuotientMap Prod.snd

Alias of isQuotientMap_snd.

theorem closure_prod_eq {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {t : Set Y} : closure (s ×ˢ t) = closure s ×ˢ closure t

theorem interior_prod_eq {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (s : Set X) (t : Set Y) : interior (s ×ˢ t) = interior s ×ˢ interior t

theorem frontier_prod_eq {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (s : Set X) (t : Set Y) : frontier (s ×ˢ t) = closure s ×ˢ frontier t ∪ frontier s ×ˢ closure t

@[simp]

theorem frontier_prod_univ_eq {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (s : Set X) : frontier (s ×ˢ Set.univ) = frontier s ×ˢ Set.univ

@[simp]

theorem frontier_univ_prod_eq {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (s : Set Y) : frontier (Set.univ ×ˢ s) = Set.univ ×ˢ frontier s

theorem map_mem_closure₂ {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y → Z} {x : X} {y : Y} {s : Set X} {t : Set Y} {u : Set Z} (hf : Continuous (Function.uncurry f)) (hx : x ∈ closure s) (hy : y ∈ closure t) (h : ∀ a ∈ s, ∀ b ∈ t, f a b ∈ u) : f x y ∈ closure u

theorem IsClosed.prod {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s₁ : Set X} {s₂ : Set Y} (h₁ : IsClosed s₁) (h₂ : IsClosed s₂) : IsClosed (s₁ ×ˢ s₂)

theorem Dense.prod {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {t : Set Y} (hs : Dense s) (ht : Dense t) : Dense (s ×ˢ t)

The product of two dense sets is a dense set.

theorem DenseRange.prodMap {Y : Type v} {Z : Type u_2} [TopologicalSpace Y] [TopologicalSpace Z] {ι : Type u_5} {κ : Type u_6} {f : ι → Y} {g : κ → Z} (hf : DenseRange f) (hg : DenseRange g) : DenseRange (Prod.map f g)

If f and g are maps with dense range, then Prod.map f g has dense range.

@[deprecated DenseRange.prodMap (since := "2024-10-05")]

theorem DenseRange.prod_map {Y : Type v} {Z : Type u_2} [TopologicalSpace Y] [TopologicalSpace Z] {ι : Type u_5} {κ : Type u_6} {f : ι → Y} {g : κ → Z} (hf : DenseRange f) (hg : DenseRange g) : DenseRange (Prod.map f g)

Alias of DenseRange.prodMap.

---

If f and g are maps with dense range, then Prod.map f g has dense range.

theorem Topology.IsInducing.prodMap {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : X → Y} {g : Z → W} (hf : IsInducing f) (hg : IsInducing g) : IsInducing (Prod.map f g)

@[deprecated Topology.IsInducing.prodMap (since := "2024-10-28")]

theorem Inducing.prodMap {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : X → Y} {g : Z → W} (hf : Topology.IsInducing f) (hg : Topology.IsInducing g) : Topology.IsInducing (Prod.map f g)

Alias of Topology.IsInducing.prodMap.

@[deprecated Topology.IsInducing.prodMap (since := "2024-10-05")]

theorem Inducing.prod_map {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : X → Y} {g : Z → W} (hf : Topology.IsInducing f) (hg : Topology.IsInducing g) : Topology.IsInducing (Prod.map f g)

Alias of Topology.IsInducing.prodMap.

@[simp]

theorem Topology.isInducing_const_prod {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {x : X} {f : Y → Z} : (IsInducing fun (x' : Y) => (x, f x')) ↔ IsInducing f

@[deprecated Topology.isInducing_const_prod (since := "2024-10-28")]

theorem inducing_const_prod {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {x : X} {f : Y → Z} : (Topology.IsInducing fun (x' : Y) => (x, f x')) ↔ Topology.IsInducing f

Alias of Topology.isInducing_const_prod.

@[simp]

theorem Topology.isInducing_prod_const {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {y : Y} {f : X → Z} : (IsInducing fun (x : X) => (f x, y)) ↔ IsInducing f

@[deprecated Topology.isInducing_prod_const (since := "2024-10-28")]

theorem inducing_prod_const {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {y : Y} {f : X → Z} : (Topology.IsInducing fun (x : X) => (f x, y)) ↔ Topology.IsInducing f

Alias of Topology.isInducing_prod_const.

theorem Topology.IsEmbedding.prodMap {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : X → Y} {g : Z → W} (hf : IsEmbedding f) (hg : IsEmbedding g) : IsEmbedding (Prod.map f g)

@[deprecated Topology.IsEmbedding.prodMap (since := "2024-10-08")]

theorem Embedding.prodMap {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : X → Y} {g : Z → W} (hf : Topology.IsEmbedding f) (hg : Topology.IsEmbedding g) : Topology.IsEmbedding (Prod.map f g)

Alias of Topology.IsEmbedding.prodMap.

@[deprecated Topology.IsEmbedding.prodMap (since := "2024-10-05")]

theorem Embedding.prod_map {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : X → Y} {g : Z → W} (hf : Topology.IsEmbedding f) (hg : Topology.IsEmbedding g) : Topology.IsEmbedding (Prod.map f g)

Alias of Topology.IsEmbedding.prodMap.

theorem IsOpenMap.prodMap {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : X → Y} {g : Z → W} (hf : IsOpenMap f) (hg : IsOpenMap g) : IsOpenMap (Prod.map f g)

@[deprecated IsOpenMap.prodMap (since := "2024-10-05")]

theorem IsOpenMap.prod {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : X → Y} {g : Z → W} (hf : IsOpenMap f) (hg : IsOpenMap g) : IsOpenMap (Prod.map f g)

Alias of IsOpenMap.prodMap.

theorem Topology.IsOpenEmbedding.prodMap {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : X → Y} {g : Z → W} (hf : IsOpenEmbedding f) (hg : IsOpenEmbedding g) : IsOpenEmbedding (Prod.map f g)

@[deprecated Topology.IsOpenEmbedding.prodMap (since := "2024-10-18")]

theorem OpenEmbedding.prodMap {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : X → Y} {g : Z → W} (hf : Topology.IsOpenEmbedding f) (hg : Topology.IsOpenEmbedding g) : Topology.IsOpenEmbedding (Prod.map f g)

Alias of Topology.IsOpenEmbedding.prodMap.

@[deprecated Topology.IsOpenEmbedding.prodMap (since := "2024-10-05")]

theorem IsOpenEmbedding.prod {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : X → Y} {g : Z → W} (hf : Topology.IsOpenEmbedding f) (hg : Topology.IsOpenEmbedding g) : Topology.IsOpenEmbedding (Prod.map f g)

Alias of Topology.IsOpenEmbedding.prodMap.

theorem isEmbedding_graph {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) : Topology.IsEmbedding fun (x : X) => (x, f x)

@[deprecated isEmbedding_graph (since := "2024-10-26")]

theorem embedding_graph {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) : Topology.IsEmbedding fun (x : X) => (x, f x)

Alias of isEmbedding_graph.

theorem isEmbedding_prodMk {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (x : X) : Topology.IsEmbedding (Prod.mk x)

@[deprecated isEmbedding_prodMk (since := "2024-10-26")]

theorem embedding_prod_mk {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (x : X) : Topology.IsEmbedding (Prod.mk x)

Alias of isEmbedding_prodMk.

theorem IsOpenQuotientMap.prodMap {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : X → Y} {g : Z → W} (hf : IsOpenQuotientMap f) (hg : IsOpenQuotientMap g) : IsOpenQuotientMap (Prod.map f g)

theorem continuous_sum_dom {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X ⊕ Y → Z} : Continuous f ↔ Continuous (f ∘ Sum.inl) ∧ Continuous (f ∘ Sum.inr)

theorem continuous_sumElim {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Z} {g : Y → Z} : Continuous (Sum.elim f g) ↔ Continuous f ∧ Continuous g

@[deprecated continuous_sumElim (since := "2025-02-20")]

theorem continuous_sum_elim {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Z} {g : Y → Z} : Continuous (Sum.elim f g) ↔ Continuous f ∧ Continuous g

Alias of continuous_sumElim.

theorem Continuous.sumElim {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Z} {g : Y → Z} (hf : Continuous f) (hg : Continuous g) : Continuous (Sum.elim f g)

@[deprecated Continuous.sumElim (since := "2025-02-20")]

theorem Continuous.sum_elim {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Z} {g : Y → Z} (hf : Continuous f) (hg : Continuous g) : Continuous (Sum.elim f g)

Alias of Continuous.sumElim.

theorem continuous_isLeft {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : Continuous Sum.isLeft

theorem continuous_isRight {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : Continuous Sum.isRight

theorem continuous_inl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : Continuous Sum.inl

theorem continuous_inr {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : Continuous Sum.inr

theorem continuous_sum_swap {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : Continuous Sum.swap

theorem isOpen_sum_iff {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set (X ⊕ Y)} : IsOpen s ↔ IsOpen (Sum.inl ⁻¹' s) ∧ IsOpen (Sum.inr ⁻¹' s)

theorem isClosed_sum_iff {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set (X ⊕ Y)} : IsClosed s ↔ IsClosed (Sum.inl ⁻¹' s) ∧ IsClosed (Sum.inr ⁻¹' s)

theorem isOpenMap_inl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : IsOpenMap Sum.inl

theorem isOpenMap_inr {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : IsOpenMap Sum.inr

theorem isClosedMap_inl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : IsClosedMap Sum.inl

theorem isClosedMap_inr {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : IsClosedMap Sum.inr

theorem Topology.IsOpenEmbedding.inl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : IsOpenEmbedding Sum.inl

@[deprecated Topology.IsOpenEmbedding.inl (since := "2024-10-30")]

theorem isOpenEmbedding_inl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : Topology.IsOpenEmbedding Sum.inl

Alias of Topology.IsOpenEmbedding.inl.

@[deprecated Topology.IsOpenEmbedding.inl (since := "2024-10-18")]

theorem openEmbedding_inl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : Topology.IsOpenEmbedding Sum.inl

Alias of Topology.IsOpenEmbedding.inl.

theorem Topology.IsOpenEmbedding.inr {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : IsOpenEmbedding Sum.inr

@[deprecated Topology.IsOpenEmbedding.inr (since := "2024-10-30")]

theorem isOpenEmbedding_inr {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : Topology.IsOpenEmbedding Sum.inr

Alias of Topology.IsOpenEmbedding.inr.

@[deprecated Topology.IsOpenEmbedding.inr (since := "2024-10-18")]

theorem openEmbedding_inr {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : Topology.IsOpenEmbedding Sum.inr

Alias of Topology.IsOpenEmbedding.inr.

theorem Topology.IsEmbedding.inl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : IsEmbedding Sum.inl

theorem Topology.IsEmbedding.inr {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : IsEmbedding Sum.inr

@[deprecated Topology.IsEmbedding.inr (since := "2024-10-26")]

theorem embedding_inr {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : Topology.IsEmbedding Sum.inr

Alias of Topology.IsEmbedding.inr.

theorem isOpen_range_inl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : IsOpen (Set.range Sum.inl)

theorem isOpen_range_inr {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : IsOpen (Set.range Sum.inr)

theorem isClosed_range_inl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : IsClosed (Set.range Sum.inl)

theorem isClosed_range_inr {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : IsClosed (Set.range Sum.inr)

theorem Topology.IsClosedEmbedding.inl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : IsClosedEmbedding Sum.inl

@[deprecated Topology.IsClosedEmbedding.inl (since := "2024-10-30")]

theorem isClosedEmbedding_inl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : Topology.IsClosedEmbedding Sum.inl

Alias of Topology.IsClosedEmbedding.inl.

@[deprecated Topology.IsClosedEmbedding.inl (since := "2024-10-20")]

theorem closedEmbedding_inl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : Topology.IsClosedEmbedding Sum.inl

Alias of Topology.IsClosedEmbedding.inl.

theorem Topology.IsClosedEmbedding.inr {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : IsClosedEmbedding Sum.inr

@[deprecated Topology.IsClosedEmbedding.inr (since := "2024-10-30")]

theorem isClosedEmbedding_inr {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : Topology.IsClosedEmbedding Sum.inr

Alias of Topology.IsClosedEmbedding.inr.

@[deprecated Topology.IsClosedEmbedding.inr (since := "2024-10-20")]

theorem closedEmbedding_inr {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : Topology.IsClosedEmbedding Sum.inr

Alias of Topology.IsClosedEmbedding.inr.

theorem nhds_inl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (x : X) : nhds (Sum.inl x) = Filter.map Sum.inl (nhds x)

theorem nhds_inr {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (y : Y) : nhds (Sum.inr y) = Filter.map Sum.inr (nhds y)

@[simp]

theorem continuous_sumMap {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace W] [TopologicalSpace Z] {f : X → Y} {g : Z → W} : Continuous (Sum.map f g) ↔ Continuous f ∧ Continuous g

@[deprecated continuous_sumMap (since := "2025-02-21")]

theorem continuous_sum_map {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace W] [TopologicalSpace Z] {f : X → Y} {g : Z → W} : Continuous (Sum.map f g) ↔ Continuous f ∧ Continuous g

Alias of continuous_sumMap.

theorem Continuous.sumMap {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace W] [TopologicalSpace Z] {f : X → Y} {g : Z → W} (hf : Continuous f) (hg : Continuous g) : Continuous (Sum.map f g)

@[deprecated Continuous.sumMap (since := "2025-02-21")]

theorem Continuous.sum_map {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace W] [TopologicalSpace Z] {f : X → Y} {g : Z → W} (hf : Continuous f) (hg : Continuous g) : Continuous (Sum.map f g)

Alias of Continuous.sumMap.

theorem isOpenMap_sum {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X ⊕ Y → Z} : IsOpenMap f ↔ (IsOpenMap fun (a : X) => f (Sum.inl a)) ∧ IsOpenMap fun (b : Y) => f (Sum.inr b)

theorem IsOpenMap.sumMap {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace W] [TopologicalSpace Z] {f : X → Y} {g : Z → W} (hf : IsOpenMap f) (hg : IsOpenMap g) : IsOpenMap (Sum.map f g)

@[simp]

theorem isOpenMap_sumElim {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Z} {g : Y → Z} : IsOpenMap (Sum.elim f g) ↔ IsOpenMap f ∧ IsOpenMap g

@[deprecated isOpenMap_sumElim (since := "2025-02-20")]

theorem isOpenMap_sum_elim {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Z} {g : Y → Z} : IsOpenMap (Sum.elim f g) ↔ IsOpenMap f ∧ IsOpenMap g

Alias of isOpenMap_sumElim.

theorem IsOpenMap.sumElim {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Z} {g : Y → Z} (hf : IsOpenMap f) (hg : IsOpenMap g) : IsOpenMap (Sum.elim f g)

@[deprecated IsOpenMap.sumElim (since := "2025-02-20")]

theorem IsOpenMap.sum_elim {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Z} {g : Y → Z} (hf : IsOpenMap f) (hg : IsOpenMap g) : IsOpenMap (Sum.elim f g)

Alias of IsOpenMap.sumElim.

theorem IsOpenEmbedding.sumElim {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Z} {g : Y → Z} (hf : Topology.IsOpenEmbedding f) (hg : Topology.IsOpenEmbedding g) (h : Function.Injective (Sum.elim f g)) : Topology.IsOpenEmbedding (Sum.elim f g)

theorem isClosedMap_sum {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X ⊕ Y → Z} : IsClosedMap f ↔ (IsClosedMap fun (a : X) => f (Sum.inl a)) ∧ IsClosedMap fun (b : Y) => f (Sum.inr b)

theorem IsClosedMap.sumMap {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace W] [TopologicalSpace Z] {f : X → Y} {g : Z → W} (hf : IsClosedMap f) (hg : IsClosedMap g) : IsClosedMap (Sum.map f g)

@[simp]

theorem isClosedMap_sumElim {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Z} {g : Y → Z} : IsClosedMap (Sum.elim f g) ↔ IsClosedMap f ∧ IsClosedMap g

theorem IsClosedMap.sumElim {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Z} {g : Y → Z} (hf : IsClosedMap f) (hg : IsClosedMap g) : IsClosedMap (Sum.elim f g)

theorem IsClosedEmbedding.sumElim {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Z} {g : Y → Z} (hf : Topology.IsClosedEmbedding f) (hg : Topology.IsClosedEmbedding g) (h : Function.Injective (Sum.elim f g)) : Topology.IsClosedEmbedding (Sum.elim f g)

def Homeomorph.sumCongr {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {X' : Type u_5} {Y' : Type u_6} [TopologicalSpace X'] [TopologicalSpace Y'] (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') : X ⊕ Y ≃ₜ X' ⊕ Y'

Sum of two homeomorphisms.

Equations

• h₁.sumCongr h₂ = { toEquiv := h₁.sumCongr h₂.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.sumCongr_symm {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {X' : Type u_5} {Y' : Type u_6} [TopologicalSpace X'] [TopologicalSpace Y'] (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') : (h₁.sumCongr h₂).symm = h₁.symm.sumCongr h₂.symm

@[simp]

theorem Homeomorph.sumCongr_refl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : (Homeomorph.refl X).sumCongr (Homeomorph.refl Y) = Homeomorph.refl (X ⊕ Y)

@[simp]

theorem Homeomorph.sumCongr_trans {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {X' : Type u_5} {Y' : Type u_6} [TopologicalSpace X'] [TopologicalSpace Y'] {X'' : Type u_7} {Y'' : Type u_8} [TopologicalSpace X''] [TopologicalSpace Y''] (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') (h₃ : X' ≃ₜ X'') (h₄ : Y' ≃ₜ Y'') : (h₁.sumCongr h₂).trans (h₃.sumCongr h₄) = (h₁.trans h₃).sumCongr (h₂.trans h₄)

def Homeomorph.prodCongr {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {X' : Type u_5} {Y' : Type u_6} [TopologicalSpace X'] [TopologicalSpace Y'] (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') : X × Y ≃ₜ X' × Y'

Product of two homeomorphisms.

Equations

• h₁.prodCongr h₂ = { toEquiv := h₁.prodCongr h₂.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.prodCongr_symm {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {X' : Type u_5} {Y' : Type u_6} [TopologicalSpace X'] [TopologicalSpace Y'] (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') : (h₁.prodCongr h₂).symm = h₁.symm.prodCongr h₂.symm

@[simp]

theorem Homeomorph.coe_prodCongr {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {X' : Type u_5} {Y' : Type u_6} [TopologicalSpace X'] [TopologicalSpace Y'] (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') : ⇑(h₁.prodCongr h₂) = Prod.map ⇑h₁ ⇑h₂

def Homeomorph.sumComm (X : Type u) (Y : Type v) [TopologicalSpace X] [TopologicalSpace Y] : X ⊕ Y ≃ₜ Y ⊕ X

X ⊕ Y is homeomorphic to Y ⊕ X.

Equations

• Homeomorph.sumComm X Y = { toEquiv := Equiv.sumComm X Y, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.sumComm_symm (X : Type u) (Y : Type v) [TopologicalSpace X] [TopologicalSpace Y] : (sumComm X Y).symm = sumComm Y X

@[simp]

theorem Homeomorph.coe_sumComm (X : Type u) (Y : Type v) [TopologicalSpace X] [TopologicalSpace Y] : ⇑(sumComm X Y) = Sum.swap

theorem Homeomorph.continuous_sumAssoc (X : Type u) (Y : Type v) (Z : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] : Continuous ⇑(Equiv.sumAssoc X Y Z)

theorem Homeomorph.continuous_sumAssoc_symm (X : Type u) (Y : Type v) (Z : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] : Continuous ⇑(Equiv.sumAssoc X Y Z).symm

def Homeomorph.sumAssoc (X : Type u) (Y : Type v) (Z : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] : (X ⊕ Y) ⊕ Z ≃ₜ X ⊕ Y ⊕ Z

(X ⊕ Y) ⊕ Z is homeomorphic to X ⊕ (Y ⊕ Z).

Equations

• Homeomorph.sumAssoc X Y Z = { toEquiv := Equiv.sumAssoc X Y Z, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.sumAssoc_toEquiv (X : Type u) (Y : Type v) (Z : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] : (sumAssoc X Y Z).toEquiv = Equiv.sumAssoc X Y Z

def Homeomorph.sumSumSumComm (X : Type u) (Y : Type v) (W : Type u_1) (Z : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace W] [TopologicalSpace Z] : (X ⊕ Y) ⊕ W ⊕ Z ≃ₜ (X ⊕ W) ⊕ Y ⊕ Z

Four-way commutativity of the disjoint union. The name matches add_add_add_comm.

Equations

• Homeomorph.sumSumSumComm X Y W Z = { toEquiv := Equiv.sumSumSumComm X Y W Z, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.sumSumSumComm_toEquiv (X : Type u) (Y : Type v) (W : Type u_1) (Z : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace W] [TopologicalSpace Z] : (sumSumSumComm W X Y Z).toEquiv = Equiv.sumSumSumComm W X Y Z

@[simp]

theorem Homeomorph.sumSumSumComm_symm (X : Type u) (Y : Type v) (W : Type u_1) (Z : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace W] [TopologicalSpace Z] : (sumSumSumComm X Y W Z).symm = sumSumSumComm X W Y Z

def Homeomorph.prodComm (X : Type u) (Y : Type v) [TopologicalSpace X] [TopologicalSpace Y] : X × Y ≃ₜ Y × X

X × Y is homeomorphic to Y × X.

Equations

• Homeomorph.prodComm X Y = { toEquiv := Equiv.prodComm X Y, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.prodComm_symm (X : Type u) (Y : Type v) [TopologicalSpace X] [TopologicalSpace Y] : (prodComm X Y).symm = prodComm Y X

@[simp]

theorem Homeomorph.coe_prodComm (X : Type u) (Y : Type v) [TopologicalSpace X] [TopologicalSpace Y] : ⇑(prodComm X Y) = Prod.swap

def Homeomorph.prodAssoc (X : Type u) (Y : Type v) (Z : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] : (X × Y) × Z ≃ₜ X × Y × Z

(X × Y) × Z is homeomorphic to X × (Y × Z).

Equations

• Homeomorph.prodAssoc X Y Z = { toEquiv := Equiv.prodAssoc X Y Z, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.prodAssoc_toEquiv (X : Type u) (Y : Type v) (Z : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] : (prodAssoc X Y Z).toEquiv = Equiv.prodAssoc X Y Z

def Homeomorph.prodProdProdComm (X : Type u) (Y : Type v) (W : Type u_1) (Z : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace W] [TopologicalSpace Z] : (X × Y) × W × Z ≃ₜ (X × W) × Y × Z

Four-way commutativity of prod. The name matches mul_mul_mul_comm.

Equations

• Homeomorph.prodProdProdComm X Y W Z = { toEquiv := Equiv.prodProdProdComm X Y W Z, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.prodProdProdComm_symm (X : Type u) (Y : Type v) (W : Type u_1) (Z : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace W] [TopologicalSpace Z] : (prodProdProdComm X Y W Z).symm = prodProdProdComm X W Y Z

def Homeomorph.prodPUnit (X : Type u) [TopologicalSpace X] : X × PUnit.{u_7 + 1} ≃ₜ X

X × {*} is homeomorphic to X.

Equations

• Homeomorph.prodPUnit X = { toEquiv := Equiv.prodPUnit X, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.prodPUnit_apply (X : Type u) [TopologicalSpace X] : ⇑(prodPUnit X) = fun (p : X × PUnit.{u_7 + 1}) => p.1

def Homeomorph.punitProd (X : Type u) [TopologicalSpace X] : PUnit.{u_7 + 1} × X ≃ₜ X

{*} × X is homeomorphic to X.

Equations

• Homeomorph.punitProd X = (Homeomorph.prodComm PUnit.{?u.17 + 1} X).trans (Homeomorph.prodPUnit X)

@[simp]

theorem Homeomorph.coe_punitProd (X : Type u) [TopologicalSpace X] : ⇑(punitProd X) = Prod.snd

def Homeomorph.sumEmpty (X : Type u) (Y : Type v) [TopologicalSpace X] [TopologicalSpace Y] [IsEmpty Y] : X ⊕ Y ≃ₜ X

The sum of X with any empty topological space is homeomorphic to X.

Equations

• Homeomorph.sumEmpty X Y = { toEquiv := Equiv.sumEmpty X Y, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.sumEmpty_apply (X : Type u) (Y : Type v) [TopologicalSpace X] [TopologicalSpace Y] [IsEmpty Y] : ⇑(sumEmpty X Y) = Sum.elim id fun (a : Y) => isEmptyElim a

def Homeomorph.emptySum (X : Type u) (Y : Type v) [TopologicalSpace X] [TopologicalSpace Y] [IsEmpty Y] : Y ⊕ X ≃ₜ X

The sum of X with any empty topological space is homeomorphic to X.

Equations

• Homeomorph.emptySum X Y = (Homeomorph.sumComm Y X).trans (Homeomorph.sumEmpty X Y)

@[simp]

theorem Homeomorph.coe_emptySum (X : Type u) (Y : Type v) [TopologicalSpace X] [TopologicalSpace Y] [IsEmpty Y] : (emptySum X Y).toEquiv = Equiv.emptySum Y X

def Homeomorph.sumProdDistrib {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] : (X ⊕ Y) × Z ≃ₜ X × Z ⊕ Y × Z

(X ⊕ Y) × Z is homeomorphic to X × Z ⊕ Y × Z.

Equations

• Homeomorph.sumProdDistrib = (Homeomorph.homeomorphOfContinuousOpen (Equiv.sumProdDistrib X Y Z).symm ⋯ ⋯).symm

@[simp]

theorem Homeomorph.sumProdDistrib_symm_apply {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (a✝ : X × Z ⊕ Y × Z) : sumProdDistrib.symm a✝ = (Equiv.sumProdDistrib X Y Z).symm a✝

@[simp]

theorem Homeomorph.sumProdDistrib_apply {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (a✝ : (X ⊕ Y) × Z) : sumProdDistrib a✝ = (Equiv.sumProdDistrib X Y Z) a✝

def Homeomorph.prodSumDistrib {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] : X × (Y ⊕ Z) ≃ₜ X × Y ⊕ X × Z

X × (Y ⊕ Z) is homeomorphic to X × Y ⊕ X × Z.

Equations

• Homeomorph.prodSumDistrib = (Homeomorph.prodComm X (Y ⊕ Z)).trans (Homeomorph.sumProdDistrib.trans ((Homeomorph.prodComm Y X).sumCongr (Homeomorph.prodComm Z X)))