Documentation

Mathlib.Topology.Constructions

Constructions of new topological spaces from old ones #

This file constructs products, sums, subtypes and quotients 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.

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, subspace, quotient space

instance instTopologicalSpaceQuot {X : Type u} {r : XXProp} [t : TopologicalSpace X] :
Equations
Equations
instance instTopologicalSpaceProd {X : Type u} {Y : Type v} [t₁ : TopologicalSpace X] [t₂ : TopologicalSpace Y] :
Equations
instance instTopologicalSpaceSum {X : Type u} {Y : Type v} [t₁ : TopologicalSpace X] [t₂ : TopologicalSpace Y] :
Equations
instance instTopologicalSpaceSigma {ι : Type u_5} {X : ιType v} [t₂ : (i : ι) → TopologicalSpace (X i)] :
Equations
instance Pi.topologicalSpace {ι : Type u_5} {Y : ιType v} [t₂ : (i : ι) → TopologicalSpace (Y i)] :
TopologicalSpace ((i : ι) → Y i)
Equations
Equations

Additive, Multiplicative #

The topology on those type synonyms is inherited without change.

Equations
  • instTopologicalSpaceAdditive = inst
Equations
  • instTopologicalSpaceMultiplicative = inst
theorem continuous_ofMul {X : Type u} [TopologicalSpace X] :
Continuous Additive.ofMul
theorem continuous_toMul {X : Type u} [TopologicalSpace X] :
Continuous Additive.toMul
theorem continuous_ofAdd {X : Type u} [TopologicalSpace X] :
Continuous Multiplicative.ofAdd
theorem continuous_toAdd {X : Type u} [TopologicalSpace X] :
Continuous Multiplicative.toAdd
theorem isOpenMap_ofMul {X : Type u} [TopologicalSpace X] :
IsOpenMap Additive.ofMul
theorem isOpenMap_toMul {X : Type u} [TopologicalSpace X] :
IsOpenMap Additive.toMul
theorem isOpenMap_ofAdd {X : Type u} [TopologicalSpace X] :
IsOpenMap Multiplicative.ofAdd
theorem isOpenMap_toAdd {X : Type u} [TopologicalSpace X] :
IsOpenMap Multiplicative.toAdd
theorem isClosedMap_ofMul {X : Type u} [TopologicalSpace X] :
IsClosedMap Additive.ofMul
theorem isClosedMap_toMul {X : Type u} [TopologicalSpace X] :
IsClosedMap Additive.toMul
theorem isClosedMap_ofAdd {X : Type u} [TopologicalSpace X] :
IsClosedMap Multiplicative.ofAdd
theorem isClosedMap_toAdd {X : Type u} [TopologicalSpace X] :
IsClosedMap Multiplicative.toAdd
theorem nhds_ofMul {X : Type u} [TopologicalSpace X] (x : X) :
nhds (Additive.ofMul x) = Filter.map (⇑Additive.ofMul) (nhds x)
theorem nhds_ofAdd {X : Type u} [TopologicalSpace X] (x : X) :
nhds (Multiplicative.ofAdd x) = Filter.map (⇑Multiplicative.ofAdd) (nhds x)
theorem nhds_toMul {X : Type u} [TopologicalSpace X] (x : Additive X) :
nhds (Additive.toMul x) = Filter.map (⇑Additive.toMul) (nhds x)
theorem nhds_toAdd {X : Type u} [TopologicalSpace X] (x : Multiplicative X) :
nhds (Multiplicative.toAdd x) = Filter.map (⇑Multiplicative.toAdd) (nhds x)

Order dual #

The topology on this type synonym is inherited without change.

Equations
  • OrderDual.instTopologicalSpace = inst
theorem continuous_toDual {X : Type u} [TopologicalSpace X] :
Continuous OrderDual.toDual
theorem continuous_ofDual {X : Type u} [TopologicalSpace X] :
Continuous OrderDual.ofDual
theorem isOpenMap_toDual {X : Type u} [TopologicalSpace X] :
IsOpenMap OrderDual.toDual
theorem isOpenMap_ofDual {X : Type u} [TopologicalSpace X] :
IsOpenMap OrderDual.ofDual
theorem isClosedMap_toDual {X : Type u} [TopologicalSpace X] :
IsClosedMap OrderDual.toDual
theorem isClosedMap_ofDual {X : Type u} [TopologicalSpace X] :
IsClosedMap OrderDual.ofDual
theorem nhds_toDual {X : Type u} [TopologicalSpace X] (x : X) :
nhds (OrderDual.toDual x) = Filter.map (⇑OrderDual.toDual) (nhds x)
theorem nhds_ofDual {X : Type u} [TopologicalSpace X] (x : X) :
nhds (OrderDual.ofDual x) = Filter.map (⇑OrderDual.ofDual) (nhds x)
instance OrderDual.instNeBotNhdsWithinIoi {X : Type u} [TopologicalSpace X] [Preorder X] {x : X} [(nhdsWithin x (Set.Iio x)).NeBot] :
(nhdsWithin (OrderDual.toDual x) (Set.Ioi (OrderDual.toDual x))).NeBot
Equations
  • = inst
instance OrderDual.instNeBotNhdsWithinIio {X : Type u} [TopologicalSpace X] [Preorder X] {x : X} [(nhdsWithin x (Set.Ioi x)).NeBot] :
(nhdsWithin (OrderDual.toDual x) (Set.Iio (OrderDual.toDual x))).NeBot
Equations
  • = inst
theorem Quotient.preimage_mem_nhds {X : Type u} [TopologicalSpace X] [s : Setoid X] {V : Set (Quotient s)} {x : X} (hs : V nhds (Quotient.mk' x)) :
Quotient.mk' ⁻¹' V nhds x
theorem Dense.quotient {X : Type u} [Setoid X] [TopologicalSpace X] {s : Set X} (H : Dense s) :
Dense (Quotient.mk' '' s)

The image of a dense set under Quotient.mk' is a dense set.

theorem DenseRange.quotient {X : Type u} {Y : Type v} [Setoid X] [TopologicalSpace X] {f : YX} (hf : DenseRange f) :
DenseRange (Quotient.mk' f)

The composition of Quotient.mk' and a function with dense range has dense range.

theorem continuous_map_of_le {α : Type u_5} [TopologicalSpace α] {s : Setoid α} {t : Setoid α} (h : s t) :
theorem continuous_map_sInf {α : Type u_5} [TopologicalSpace α] {S : Set (Setoid α)} {s : Setoid α} (h : s S) :
Equations
  • =
Equations
  • =
instance Sigma.discreteTopology {ι : Type u_5} {Y : ιType v} [(i : ι) → TopologicalSpace (Y i)] [h : ∀ (i : ι), DiscreteTopology (Y i)] :
Equations
  • =
@[simp]
theorem comap_nhdsWithin_range {α : Type u_5} {β : Type u_6} [TopologicalSpace β] (f : αβ) (y : β) :
theorem mem_nhds_subtype {X : Type u} [TopologicalSpace X] (s : Set X) (x : { x : X // x s }) (t : Set { x : X // x s }) :
t nhds x unhds x, Subtype.val ⁻¹' u t
theorem nhds_subtype {X : Type u} [TopologicalSpace X] (s : Set X) (x : { x : X // x s }) :
nhds x = Filter.comap Subtype.val (nhds x)
theorem nhds_subtype_eq_comap_nhdsWithin {X : Type u} [TopologicalSpace X] (s : Set X) (x : { x : X // x s }) :
nhds x = Filter.comap Subtype.val (nhdsWithin (↑x) s)
theorem nhdsWithin_subtype_eq_bot_iff {X : Type u} [TopologicalSpace X] {s : Set X} {t : Set X} {x : s} :
nhdsWithin x (Subtype.val ⁻¹' t) = nhdsWithin (↑x) t Filter.principal s =
theorem nhds_ne_subtype_neBot_iff {X : Type u} [TopologicalSpace X] {S : Set X} {x : S} :
(nhdsWithin x {x}).NeBot (nhdsWithin x {x} Filter.principal S).NeBot
def CofiniteTopology (X : Type u_5) :
Type u_5

A type synonym equipped with the topology whose open sets are the empty set and the sets with finite complements.

Equations
Instances For

    The identity equivalence between `` and CofiniteTopology .

    Equations
    Instances For
      Equations
      • CofiniteTopology.instInhabited = { default := CofiniteTopology.of default }
      Equations
      • CofiniteTopology.instTopologicalSpace = { IsOpen := fun (s : Set (CofiniteTopology X)) => s.Nonemptys.Finite, isOpen_univ := , isOpen_inter := , isOpen_sUnion := }
      theorem CofiniteTopology.isOpen_iff {X : Type u} {s : Set (CofiniteTopology X)} :
      IsOpen s s.Nonemptys.Finite
      theorem CofiniteTopology.isClosed_iff {X : Type u} {s : Set (CofiniteTopology X)} :
      IsClosed s s = Set.univ s.Finite
      theorem CofiniteTopology.nhds_eq {X : Type u} (x : CofiniteTopology X) :
      nhds x = pure x Filter.cofinite
      @[simp]
      theorem continuous_prod_mk {X : Type u} {Y : Type v} {Z : Type u_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : XY} {g : XZ} :
      (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_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : XY × 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_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : XZ} (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_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : XY × 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_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : XZ} {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_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : XZ} {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_1} [TopologicalSpace Y] [TopologicalSpace Z] {X : Type u_5} {l : Filter X} {f : XY × Z} {p : Y × Z} (h : Filter.Tendsto f l (nhds p)) :
      Filter.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_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : XY × 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_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : YZ} (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_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : XY × 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_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : YZ} {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_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : YZ} {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_1} [TopologicalSpace Y] [TopologicalSpace Z] {X : Type u_5} {l : Filter X} {f : XY × Z} {p : Y × Z} (h : Filter.Tendsto f l (nhds p)) :
      Filter.Tendsto (fun (a : X) => (f a).2) l (nhds p.2)
      theorem Continuous.prod_mk {X : Type u} {Y : Type v} {Z : Type u_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : ZX} {g : ZY} (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_1} [TopologicalSpace X] [TopologicalSpace Z] {α : Type u_5} {f : XαZ} {s : Set α} {t : Set Z} (ht : IsClosed t) (hf : as, 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} {Z : Type u_1} {W : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {g : X × YZ} (hg : Continuous g) {e : WX} (he : Continuous e) {f : WY} (hf : Continuous f) :
      Continuous fun (w : W) => g (e w, f w)
      theorem Continuous.comp₃ {X : Type u} {Y : Type v} {Z : Type u_1} {W : Type u_2} {ε : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] [TopologicalSpace ε] {g : X × Y × Zε} (hg : Continuous g) {e : WX} (he : Continuous e) {f : WY} (hf : Continuous f) {k : WZ} (hk : Continuous k) :
      Continuous fun (w : W) => g (e w, f w, k w)
      theorem Continuous.comp₄ {X : Type u} {Y : Type v} {Z : Type u_1} {W : 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 : WX} (he : Continuous e) {f : WY} (hf : Continuous f) {k : WZ} (hk : Continuous k) {l : Wζ} (hl : Continuous l) :
      Continuous fun (w : W) => g (e w, f w, k w, l w)
      theorem Continuous.prod_map {X : Type u} {Y : Type v} {Z : Type u_1} {W : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : ZX} {g : WY} (hf : Continuous f) (hg : Continuous g) :
      Continuous fun (p : Z × W) => (f p.1, g p.2)
      theorem continuous_inf_dom_left₂ {X : Type u_5} {Y : Type u_6} {Z : Type u_7} {f : XYZ} {ta1 : TopologicalSpace X} {ta2 : TopologicalSpace X} {tb1 : TopologicalSpace Y} {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 : XYZ} {ta1 : TopologicalSpace X} {ta2 : TopologicalSpace X} {tb1 : TopologicalSpace Y} {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 : XYZ} {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 : XProp} {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 : YProp} {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 : XProp} {x : X} (hx : ∀ᶠ (x : X) in nhds x, px x) {py : YProp} {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 Continuous.uncurry_left {X : Type u} {Y : Type v} {Z : Type u_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : XYZ} (x : X) (h : Continuous (Function.uncurry f)) :
      theorem Continuous.uncurry_right {X : Type u} {Y : Type v} {Z : Type u_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : XYZ} (y : Y) (h : Continuous (Function.uncurry f)) :
      Continuous fun (a : X) => f a y
      @[deprecated Continuous.uncurry_left]
      theorem continuous_uncurry_left {X : Type u} {Y : Type v} {Z : Type u_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : XYZ} (x : X) (h : Continuous (Function.uncurry f)) :

      Alias of Continuous.uncurry_left.

      @[deprecated Continuous.uncurry_right]
      theorem continuous_uncurry_right {X : Type u} {Y : Type v} {Z : Type u_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : XYZ} (y : Y) (h : Continuous (Function.uncurry f)) :
      Continuous fun (a : X) => f a y

      Alias of Continuous.uncurry_right.

      theorem continuous_curry {X : Type u} {Y : Type v} {Z : Type u_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {g : X × YZ} (x : X) (h : Continuous g) :
      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
      Equations
      • =
      instance Prod.instNeBotNhdsWithinIoi {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [Preorder X] [Preorder Y] {x : X × Y} [(nhdsWithin x.1 (Set.Ioi x.1)).NeBot] [(nhdsWithin x.2 (Set.Ioi x.2)).NeBot] :
      (nhdsWithin x (Set.Ioi x)).NeBot
      Equations
      • =
      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) unhds x, vnhds 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) unhdsWithin x tx, vnhdsWithin 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 : ιXProp} {py : ιYProp} {sx : ιXSet X} {sy : ιYSet 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 : ιXProp} {pY : ιYProp} {sx : ιXSet X} {sy : ιYSet 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 MapClusterPt.curry_prodMap {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {α : Type u_5} {β : Type u_6} {f : αX} {g : βY} {la : Filter α} {lb : Filter β} {x : X} {y : Y} (hf : MapClusterPt x la f) (hg : MapClusterPt y lb g) :
      MapClusterPt (x, y) (la.curry lb) (Prod.map f g)
      theorem MapClusterPt.prodMap {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {α : Type u_5} {β : Type u_6} {f : αX} {g : βY} {la : Filter α} {lb : Filter β} {x : X} {y : Y} (hf : MapClusterPt x la f) (hg : MapClusterPt y lb g) :
      MapClusterPt (x, y) (la ×ˢ lb) (Prod.map f g)
      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_1} [TopologicalSpace Y] [TopologicalSpace Z] {X : Type u_5} (seq : XY × 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)
      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 Filter.Eventually.prod_nhds {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {p : XProp} {q : YProp} {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 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 : Filter.Tendsto mx f (nhds x)) (hy : Filter.Tendsto my f (nhds y)) :
      Filter.Tendsto (fun (c : γ) => (mx c, my c)) f (nhds (x, y))
      theorem Filter.Eventually.curry_nhds {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {p : X × YProp} {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_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : XY} {g : XZ} {x : X} (hf : ContinuousAt f x) (hg : ContinuousAt g x) :
      ContinuousAt (fun (x : X) => (f x, g x)) x
      theorem ContinuousAt.prod_map {X : Type u} {Y : Type v} {Z : Type u_1} {W : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : XZ} {g : YW} {p : X × Y} (hf : ContinuousAt f p.1) (hg : ContinuousAt g p.2) :
      ContinuousAt (fun (p : X × Y) => (f p.1, g p.2)) p
      theorem ContinuousAt.prod_map' {X : Type u} {Y : Type v} {Z : Type u_1} {W : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : XZ} {g : YW} {x : X} {y : Y} (hf : ContinuousAt f x) (hg : ContinuousAt g y) :
      ContinuousAt (fun (p : X × Y) => (f p.1, g p.2)) (x, y)
      theorem ContinuousAt.comp₂ {X : Type u} {Y : Type v} {Z : Type u_1} {W : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : Y × ZW} {g : XY} {h : XZ} {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} {Z : Type u_1} {W : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : Y × ZW} {g : XY} {h : XZ} {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_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X × YZ} (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_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X × YZ} (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_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X × YZ} (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_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X × YZ} (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_2} [TopologicalSpace Y] [TopologicalSpace W] {X : Type u_5} {Z : Type u_6} (f : XY) (g : ZW) :
      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} :

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

      theorem closure_prod_eq {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {t : Set Y} :
      theorem interior_prod_eq {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (s : Set X) (t : Set Y) :
      @[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_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : XYZ} {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 : as, bt, 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.prod_map {Y : Type v} {Z : Type u_1} [TopologicalSpace Y] [TopologicalSpace Z] {ι : Type u_5} {κ : Type u_6} {f : ιY} {g : κZ} (hf : DenseRange f) (hg : DenseRange g) :

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

      theorem Inducing.prod_map {X : Type u} {Y : Type v} {Z : Type u_1} {W : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : XY} {g : ZW} (hf : Inducing f) (hg : Inducing g) :
      @[simp]
      theorem inducing_const_prod {X : Type u} {Y : Type v} {Z : Type u_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {x : X} {f : YZ} :
      (Inducing fun (x' : Y) => (x, f x')) Inducing f
      @[simp]
      theorem inducing_prod_const {X : Type u} {Y : Type v} {Z : Type u_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {y : Y} {f : XZ} :
      (Inducing fun (x : X) => (f x, y)) Inducing f
      theorem Embedding.prod_map {X : Type u} {Y : Type v} {Z : Type u_1} {W : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : XY} {g : ZW} (hf : Embedding f) (hg : Embedding g) :
      theorem IsOpenMap.prod {X : Type u} {Y : Type v} {Z : Type u_1} {W : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : XY} {g : ZW} (hf : IsOpenMap f) (hg : IsOpenMap g) :
      IsOpenMap fun (p : X × Z) => (f p.1, g p.2)
      theorem OpenEmbedding.prod {X : Type u} {Y : Type v} {Z : Type u_1} {W : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : XY} {g : ZW} (hf : OpenEmbedding f) (hg : OpenEmbedding g) :
      OpenEmbedding fun (x : X × Z) => (f x.1, g x.2)
      theorem embedding_graph {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (hf : Continuous f) :
      Embedding fun (x : X) => (x, f x)
      theorem IsOpenQuotientMap.prodMap {X : Type u} {Y : Type v} {Z : Type u_1} {W : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : XY} {g : ZW} (hf : IsOpenQuotientMap f) (hg : IsOpenQuotientMap g) :
      theorem continuous_bool_rng {X : Type u} [TopologicalSpace X] {f : XBool} (b : Bool) :
      theorem continuous_sum_dom {X : Type u} {Y : Type v} {Z : Type u_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X YZ} :
      Continuous f Continuous (f Sum.inl) Continuous (f Sum.inr)
      theorem continuous_sum_elim {X : Type u} {Y : Type v} {Z : Type u_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : XZ} {g : YZ} :
      theorem Continuous.sum_elim {X : Type u} {Y : Type v} {Z : Type u_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : XZ} {g : YZ} (hf : Continuous f) (hg : Continuous g) :
      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 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 embedding_inl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] :
      Embedding Sum.inl
      theorem embedding_inr {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] :
      Embedding Sum.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_sum_map {X : Type u} {Y : Type v} {Z : Type u_1} {W : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : XY} {g : ZW} :
      theorem Continuous.sum_map {X : Type u} {Y : Type v} {Z : Type u_1} {W : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : XY} {g : ZW} (hf : Continuous f) (hg : Continuous g) :
      theorem isOpenMap_sum {X : Type u} {Y : Type v} {Z : Type u_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X YZ} :
      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} {Z : Type u_1} {W : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : XY} {g : ZW} (hf : IsOpenMap f) (hg : IsOpenMap g) :
      @[simp]
      theorem isOpenMap_sum_elim {X : Type u} {Y : Type v} {Z : Type u_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : XZ} {g : YZ} :
      theorem IsOpenMap.sum_elim {X : Type u} {Y : Type v} {Z : Type u_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : XZ} {g : YZ} (hf : IsOpenMap f) (hg : IsOpenMap g) :
      theorem isClosedMap_sum {X : Type u} {Y : Type v} {Z : Type u_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X YZ} :
      IsClosedMap f (IsClosedMap fun (a : X) => f (Sum.inl a)) IsClosedMap fun (b : Y) => f (Sum.inr b)
      theorem inducing_subtype_val {Y : Type v} [TopologicalSpace Y] {t : Set Y} :
      Inducing Subtype.val
      theorem Inducing.of_codRestrict {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} {t : Set Y} (ht : ∀ (x : X), f x t) (h : Inducing (Set.codRestrict f t ht)) :
      theorem embedding_subtype_val {X : Type u} [TopologicalSpace X] {p : XProp} :
      Embedding Subtype.val
      theorem closedEmbedding_subtype_val {X : Type u} [TopologicalSpace X] {p : XProp} (h : IsClosed {a : X | p a}) :
      ClosedEmbedding Subtype.val
      theorem continuous_subtype_val {X : Type u} [TopologicalSpace X] {p : XProp} :
      Continuous Subtype.val
      theorem Continuous.subtype_val {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {p : XProp} {f : YSubtype p} (hf : Continuous f) :
      Continuous fun (x : Y) => (f x)
      theorem IsOpen.openEmbedding_subtype_val {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsOpen s) :
      OpenEmbedding Subtype.val
      theorem IsOpen.isOpenMap_subtype_val {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsOpen s) :
      IsOpenMap Subtype.val
      theorem IsOpenMap.restrict {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (hf : IsOpenMap f) {s : Set X} (hs : IsOpen s) :
      IsOpenMap (s.restrict f)
      theorem IsClosed.isClosedMap_subtype_val {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsClosed s) :
      IsClosedMap Subtype.val
      theorem Continuous.subtype_mk {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {p : XProp} {f : YX} (h : Continuous f) (hp : ∀ (x : Y), p (f x)) :
      Continuous fun (x : Y) => f x,
      theorem Continuous.subtype_map {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {p : XProp} {f : XY} (h : Continuous f) {q : YProp} (hpq : ∀ (x : X), p xq (f x)) :
      theorem continuous_inclusion {X : Type u} [TopologicalSpace X] {s : Set X} {t : Set X} (h : s t) :
      theorem continuousAt_subtype_val {X : Type u} [TopologicalSpace X] {p : XProp} {x : Subtype p} :
      ContinuousAt Subtype.val x
      theorem Subtype.dense_iff {X : Type u} [TopologicalSpace X] {s : Set X} {t : Set s} :
      Dense t s closure (Subtype.val '' t)
      theorem map_nhds_subtype_val {X : Type u} [TopologicalSpace X] {s : Set X} (x : s) :
      Filter.map Subtype.val (nhds x) = nhdsWithin (↑x) s
      theorem map_nhds_subtype_coe_eq_nhds {X : Type u} [TopologicalSpace X] {p : XProp} {x : X} (hx : p x) (h : ∀ᶠ (x : X) in nhds x, p x) :
      Filter.map Subtype.val (nhds x, hx) = nhds x
      theorem nhds_subtype_eq_comap {X : Type u} [TopologicalSpace X] {p : XProp} {x : X} {h : p x} :
      nhds x, h = Filter.comap Subtype.val (nhds x)
      theorem tendsto_subtype_rng {X : Type u} [TopologicalSpace X] {Y : Type u_5} {p : XProp} {l : Filter Y} {f : YSubtype p} {x : Subtype p} :
      Filter.Tendsto f l (nhds x) Filter.Tendsto (fun (x : Y) => (f x)) l (nhds x)
      theorem closure_subtype {X : Type u} [TopologicalSpace X] {p : XProp} {x : { a : X // p a }} {s : Set { a : X // p a }} :
      x closure s x closure (Subtype.val '' s)
      @[simp]
      theorem continuousAt_codRestrict_iff {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} {t : Set Y} (h1 : ∀ (x : X), f x t) {x : X} :
      theorem ContinuousAt.codRestrict {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} {t : Set Y} (h1 : ∀ (x : X), f x t) {x : X} :

      Alias of the reverse direction of continuousAt_codRestrict_iff.

      theorem ContinuousAt.restrict {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} {s : Set X} {t : Set Y} (h1 : Set.MapsTo f s t) {x : s} (h2 : ContinuousAt f x) :
      theorem ContinuousAt.restrictPreimage {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} {s : Set Y} {x : (f ⁻¹' s)} (h : ContinuousAt f x) :
      ContinuousAt (s.restrictPreimage f) x
      theorem Continuous.codRestrict {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} {s : Set Y} (hf : Continuous f) (hs : ∀ (a : X), f a s) :
      theorem Continuous.restrict {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} {s : Set X} {t : Set Y} (h1 : Set.MapsTo f s t) (h2 : Continuous f) :
      theorem Continuous.restrictPreimage {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} {s : Set Y} (h : Continuous f) :
      Continuous (s.restrictPreimage f)
      theorem Inducing.codRestrict {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {e : XY} (he : Inducing e) {s : Set Y} (hs : ∀ (x : X), e x s) :
      theorem Embedding.codRestrict {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {e : XY} (he : Embedding e) (s : Set Y) (hs : ∀ (x : X), e x s) :
      theorem embedding_inclusion {X : Type u} [TopologicalSpace X] {s : Set X} {t : Set X} (h : s t) :
      theorem DiscreteTopology.of_subset {X : Type u_5} [TopologicalSpace X] {s : Set X} {t : Set X} :
      DiscreteTopology st sDiscreteTopology t

      Let s, t ⊆ X be two subsets of a topological space X. If t ⊆ s and the topology induced by Xon s is discrete, then also the topology induces on t is discrete.

      Let s be a discrete subset of a topological space. Then the preimage of s by a continuous injective map is also discrete.

      theorem QuotientMap.restrictPreimage_isOpen {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (hf : QuotientMap f) {s : Set Y} (hs : IsOpen s) :
      QuotientMap (s.restrictPreimage f)

      If f : X → Y is a quotient map, then its restriction to the preimage of an open set is a quotient map too.

      theorem isClosed_preimage_val {X : Type u} [TopologicalSpace X] {s : Set X} {t : Set X} :
      IsClosed (Subtype.val ⁻¹' t) s closure (s t) t
      theorem quotientMap_quot_mk {X : Type u} [TopologicalSpace X] {r : XXProp} :
      theorem continuous_quot_mk {X : Type u} [TopologicalSpace X] {r : XXProp} :
      theorem continuous_quot_lift {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {r : XXProp} {f : XY} (hr : ∀ (a b : X), r a bf a = f b) (h : Continuous f) :
      theorem quotientMap_quotient_mk' {X : Type u} [TopologicalSpace X] {s : Setoid X} :
      QuotientMap Quotient.mk'
      theorem continuous_quotient_mk' {X : Type u} [TopologicalSpace X] {s : Setoid X} :
      Continuous Quotient.mk'
      theorem Continuous.quotient_lift {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Setoid X} {f : XY} (h : Continuous f) (hs : ∀ (a b : X), a bf a = f b) :
      theorem Continuous.quotient_liftOn' {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Setoid X} {f : XY} (h : Continuous f) (hs : ∀ (a b : X), Setoid.r a bf a = f b) :
      Continuous fun (x : Quotient s) => x.liftOn' f hs
      theorem Continuous.quotient_map' {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Setoid X} {t : Setoid Y} {f : XY} (hf : Continuous f) (H : (Setoid.r Setoid.r) f f) :
      theorem continuous_pi_iff {X : Type u} {ι : Type u_5} {π : ιType u_6} [TopologicalSpace X] [T : (i : ι) → TopologicalSpace (π i)] {f : X(i : ι) → π i} :
      Continuous f ∀ (i : ι), Continuous fun (a : X) => f a i
      theorem continuous_pi {X : Type u} {ι : Type u_5} {π : ιType u_6} [TopologicalSpace X] [T : (i : ι) → TopologicalSpace (π i)] {f : X(i : ι) → π i} (h : ∀ (i : ι), Continuous fun (a : X) => f a i) :
      theorem continuous_apply {ι : Type u_5} {π : ιType u_6} [T : (i : ι) → TopologicalSpace (π i)] (i : ι) :
      Continuous fun (p : (i : ι) → π i) => p i
      theorem continuous_apply_apply {ι : Type u_5} {κ : Type u_7} {ρ : κιType u_8} [(j : κ) → (i : ι) → TopologicalSpace (ρ j i)] (j : κ) (i : ι) :
      Continuous fun (p : (j : κ) → (i : ι) → ρ j i) => p j i
      theorem continuousAt_apply {ι : Type u_5} {π : ιType u_6} [T : (i : ι) → TopologicalSpace (π i)] (i : ι) (x : (i : ι) → π i) :
      ContinuousAt (fun (p : (i : ι) → π i) => p i) x
      theorem Filter.Tendsto.apply_nhds {Y : Type v} {ι : Type u_5} {π : ιType u_6} [T : (i : ι) → TopologicalSpace (π i)] {l : Filter Y} {f : Y(i : ι) → π i} {x : (i : ι) → π i} (h : Filter.Tendsto f l (nhds x)) (i : ι) :
      Filter.Tendsto (fun (a : Y) => f a i) l (nhds (x i))
      theorem nhds_pi {ι : Type u_5} {π : ιType u_6} [T : (i : ι) → TopologicalSpace (π i)] {a : (i : ι) → π i} :
      nhds a = Filter.pi fun (i : ι) => nhds (a i)
      theorem tendsto_pi_nhds {Y : Type v} {ι : Type u_5} {π : ιType u_6} [T : (i : ι) → TopologicalSpace (π i)] {f : Y(i : ι) → π i} {g : (i : ι) → π i} {u : Filter Y} :
      Filter.Tendsto f u (nhds g) ∀ (x : ι), Filter.Tendsto (fun (i : Y) => f i x) u (nhds (g x))
      theorem continuousAt_pi {X : Type u} {ι : Type u_5} {π : ιType u_6} [TopologicalSpace X] [T : (i : ι) → TopologicalSpace (π i)] {f : X(i : ι) → π i} {x : X} :
      ContinuousAt f x ∀ (i : ι), ContinuousAt (fun (y : X) => f y i) x
      theorem continuousAt_pi' {X : Type u} {ι : Type u_5} {π : ιType u_6} [TopologicalSpace X] [T : (i : ι) → TopologicalSpace (π i)] {f : X(i : ι) → π i} {x : X} (hf : ∀ (i : ι), ContinuousAt (fun (y : X) => f y i) x) :
      theorem Pi.continuous_precomp' {ι : Type u_5} {π : ιType u_6} [T : (i : ι) → TopologicalSpace (π i)] {ι' : Type u_8} (φ : ι'ι) :
      Continuous fun (f : (i : ι) → π i) (j : ι') => f (φ j)
      theorem Pi.continuous_precomp {X : Type u} {ι : Type u_5} [TopologicalSpace X] {ι' : Type u_8} (φ : ι'ι) :
      Continuous fun (x : ιX) => x φ
      theorem Pi.continuous_postcomp' {ι : Type u_5} {π : ιType u_6} [T : (i : ι) → TopologicalSpace (π i)] {X : ιType u_8} [(i : ι) → TopologicalSpace (X i)] {g : (i : ι) → π iX i} (hg : ∀ (i : ι), Continuous (g i)) :
      Continuous fun (f : (i : ι) → π i) (i : ι) => g i (f i)
      theorem Pi.continuous_postcomp {X : Type u} {Y : Type v} {ι : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] {g : XY} (hg : Continuous g) :
      Continuous fun (x : ιX) => g x
      theorem Pi.induced_precomp' {ι : Type u_5} {π : ιType u_6} [T : (i : ι) → TopologicalSpace (π i)] {ι' : Type u_8} (φ : ι'ι) :
      TopologicalSpace.induced (fun (f : (i : ι) → π i) (j : ι') => f (φ j)) Pi.topologicalSpace = ⨅ (i' : ι'), TopologicalSpace.induced (Function.eval (φ i')) (T (φ i'))
      theorem Pi.induced_precomp {Y : Type v} {ι : Type u_5} [TopologicalSpace Y] {ι' : Type u_8} (φ : ι'ι) :
      TopologicalSpace.induced (fun (x : ιY) => x φ) Pi.topologicalSpace = ⨅ (i' : ι'), TopologicalSpace.induced (Function.eval (φ i')) inst✝
      theorem Pi.continuous_restrict {ι : Type u_5} {π : ιType u_6} [T : (i : ι) → TopologicalSpace (π i)] (S : Set ι) :
      Continuous S.restrict
      theorem Pi.continuous_restrict₂ {ι : Type u_5} {π : ιType u_6} [T : (i : ι) → TopologicalSpace (π i)] {s : Set ι} {t : Set ι} (hst : s t) :
      theorem Finset.continuous_restrict {ι : Type u_5} {π : ιType u_6} [T : (i : ι) → TopologicalSpace (π i)] (s : Finset ι) :
      Continuous s.restrict
      theorem Finset.continuous_restrict₂ {ι : Type u_5} {π : ιType u_6} [T : (i : ι) → TopologicalSpace (π i)] {s : Finset ι} {t : Finset ι} (hst : s t) :
      theorem Pi.continuous_restrict_apply {X : Type u} [TopologicalSpace X] {Z : Type u_8} [TopologicalSpace Z] (s : Set X) {f : XZ} (hf : Continuous f) :
      Continuous (s.restrict f)
      theorem Pi.continuous_restrict₂_apply {X : Type u} [TopologicalSpace X] {Z : Type u_8} [TopologicalSpace Z] {s : Set X} {t : Set X} (hst : s t) {f : tZ} (hf : Continuous f) :
      theorem Finset.continuous_restrict_apply {X : Type u} [TopologicalSpace X] {Z : Type u_8} [TopologicalSpace Z] (s : Finset X) {f : XZ} (hf : Continuous f) :
      Continuous (s.restrict f)
      theorem Finset.continuous_restrict₂_apply {X : Type u} [TopologicalSpace X] {Z : Type u_8} [TopologicalSpace Z] {s : Finset X} {t : Finset X} (hst : s t) {f : { x : X // x t }Z} (hf : Continuous f) :
      theorem Pi.induced_restrict {ι : Type u_5} {π : ιType u_6} [T : (i : ι) → TopologicalSpace (π i)] (S : Set ι) :
      TopologicalSpace.induced S.restrict Pi.topologicalSpace = iS, TopologicalSpace.induced (Function.eval i) (T i)
      theorem Pi.induced_restrict_sUnion {ι : Type u_5} {π : ιType u_6} [T : (i : ι) → TopologicalSpace (π i)] (𝔖 : Set (Set ι)) :
      TopologicalSpace.induced (⋃₀ 𝔖).restrict Pi.topologicalSpace = S𝔖, TopologicalSpace.induced S.restrict Pi.topologicalSpace
      theorem Filter.Tendsto.update {Y : Type v} {ι : Type u_5} {π : ιType u_6} [T : (i : ι) → TopologicalSpace (π i)] [DecidableEq ι] {l : Filter Y} {f : Y(i : ι) → π i} {x : (i : ι) → π i} (hf : Filter.Tendsto f l (nhds x)) (i : ι) {g : Yπ i} {xi : π i} (hg : Filter.Tendsto g l (nhds xi)) :
      Filter.Tendsto (fun (a : Y) => Function.update (f a) i (g a)) l (nhds (Function.update x i xi))
      theorem ContinuousAt.update {X : Type u} {ι : Type u_5} {π : ιType u_6} [TopologicalSpace X] [T : (i : ι) → TopologicalSpace (π i)] {f : X(i : ι) → π i} [DecidableEq ι] {x : X} (hf : ContinuousAt f x) (i : ι) {g : Xπ i} (hg : ContinuousAt g x) :
      ContinuousAt (fun (a : X) => Function.update (f a) i (g a)) x
      theorem Continuous.update {X : Type u} {ι : Type u_5} {π : ιType u_6} [TopologicalSpace X] [T : (i : ι) → TopologicalSpace (π i)] {f : X(i : ι) → π i} [DecidableEq ι] (hf : Continuous f) (i : ι) {g : Xπ i} (hg : Continuous g) :
      Continuous fun (a : X) => Function.update (f a) i (g a)
      theorem continuous_update {ι : Type u_5} {π : ιType u_6} [T : (i : ι) → TopologicalSpace (π i)] [DecidableEq ι] (i : ι) :
      Continuous fun (f : ((j : ι) → π j) × π i) => Function.update f.1 i f.2

      Function.update f i x is continuous in (f, x).

      theorem continuous_single {ι : Type u_5} {π : ιType u_6} [T : (i : ι) → TopologicalSpace (π i)] [(i : ι) → Zero (π i)] [DecidableEq ι] (i : ι) :
      Continuous fun (x : π i) => Pi.single i x

      Pi.single i x is continuous in x.

      theorem continuous_mulSingle {ι : Type u_5} {π : ιType u_6} [T : (i : ι) → TopologicalSpace (π i)] [(i : ι) → One (π i)] [DecidableEq ι] (i : ι) :
      Continuous fun (x : π i) => Pi.mulSingle i x

      Pi.mulSingle i x is continuous in x.

      theorem Filter.Tendsto.fin_insertNth {Y : Type v} {n : } {π : Fin (n + 1)Type u_9} [(i : Fin (n + 1)) → TopologicalSpace (π i)] (i : Fin (n + 1)) {f : Yπ i} {l : Filter Y} {x : π i} (hf : Filter.Tendsto f l (nhds x)) {g : Y(j : Fin n) → π (i.succAbove j)} {y : (j : Fin n) → π (i.succAbove j)} (hg : Filter.Tendsto g l (nhds y)) :
      Filter.Tendsto (fun (a : Y) => i.insertNth (f a) (g a)) l (nhds (i.insertNth x y))
      theorem ContinuousAt.fin_insertNth {X : Type u} [TopologicalSpace X] {n : } {π : Fin (n + 1)Type u_9} [(i : Fin (n + 1)) → TopologicalSpace (π i)] (i : Fin (n + 1)) {f : Xπ i} {x : X} (hf : ContinuousAt f x) {g : X(j : Fin n) → π (i.succAbove j)} (hg : ContinuousAt g x) :
      ContinuousAt (fun (a : X) => i.insertNth (f a) (g a)) x
      theorem Continuous.fin_insertNth {X : Type u} [TopologicalSpace X] {n : } {π : Fin (n + 1)Type u_9} [(i : Fin (n + 1)) → TopologicalSpace (π i)] (i : Fin (n + 1)) {f : Xπ i} (hf : Continuous f) {g : X(j : Fin n) → π (i.succAbove j)} (hg : Continuous g) :
      Continuous fun (a : X) => i.insertNth (f a) (g a)
      theorem isOpen_set_pi {ι : Type u_5} {π : ιType u_6} [T : (i : ι) → TopologicalSpace (π i)] {i : Set ι} {s : (a : ι) → Set (π a)} (hi : i.Finite) (hs : ai, IsOpen (s a)) :
      IsOpen (i.pi s)
      theorem isOpen_pi_iff {ι : Type u_5} {π : ιType u_6} [T : (i : ι) → TopologicalSpace (π i)] {s : Set ((a : ι) → π a)} :
      IsOpen s fs, ∃ (I : Finset ι) (u : (a : ι) → Set (π a)), (∀ aI, IsOpen (u a) f a u a) (↑I).pi u s
      theorem isOpen_pi_iff' {ι : Type u_5} {π : ιType u_6} [T : (i : ι) → TopologicalSpace (π i)] [Finite ι] {s : Set ((a : ι) → π a)} :
      IsOpen s fs, ∃ (u : (a : ι) → Set (π a)), (∀ (a : ι), IsOpen (u a) f a u a) Set.univ.pi u s
      theorem isClosed_set_pi {ι : Type u_5} {π : ιType u_6} [T : (i : ι) → TopologicalSpace (π i)] {i : Set ι} {s : (a : ι) → Set (π a)} (hs : ai, IsClosed (s a)) :
      IsClosed (i.pi s)
      theorem mem_nhds_of_pi_mem_nhds {ι : Type u_5} {π : ιType u_6} [T : (i : ι) → TopologicalSpace (π i)] {I : Set ι} {s : (i : ι) → Set (π i)} (a : (i : ι) → π i) (hs : I.pi s nhds a) {i : ι} (hi : i I) :
      s i nhds (a i)
      theorem set_pi_mem_nhds {ι : Type u_5} {π : ιType u_6} [T : (i : ι) → TopologicalSpace (π i)] {i : Set ι} {s : (a : ι) → Set (π a)} {x : (a : ι) → π a} (hi : i.Finite) (hs : ai, s a nhds (x a)) :
      i.pi s nhds x
      theorem set_pi_mem_nhds_iff {ι : Type u_5} {π : ιType u_6} [T : (i : ι) → TopologicalSpace (π i)] {I : Set ι} (hI : I.Finite) {s : (i : ι) → Set (π i)} (a : (i : ι) → π i) :
      I.pi s nhds a iI, s i nhds (a i)
      theorem interior_pi_set {ι : Type u_5} {π : ιType u_6} [T : (i : ι) → TopologicalSpace (π i)] {I : Set ι} (hI : I.Finite) {s : (i : ι) → Set (π i)} :
      interior (I.pi s) = I.pi fun (i : ι) => interior (s i)
      theorem exists_finset_piecewise_mem_of_mem_nhds {ι : Type u_5} {π : ιType u_6} [T : (i : ι) → TopologicalSpace (π i)] [DecidableEq ι] {s : Set ((a : ι) → π a)} {x : (a : ι) → π a} (hs : s nhds x) (y : (a : ι) → π a) :
      ∃ (I : Finset ι), I.piecewise x y s
      theorem pi_generateFrom_eq {ι : Type u_5} {π : ιType u_9} {g : (a : ι) → Set (Set (π a))} :
      Pi.topologicalSpace = TopologicalSpace.generateFrom {t : Set ((i : ι) → π i) | ∃ (s : (a : ι) → Set (π a)) (i : Finset ι), (∀ ai, s a g a) t = (↑i).pi s}
      theorem pi_eq_generateFrom {ι : Type u_5} {π : ιType u_6} [T : (i : ι) → TopologicalSpace (π i)] :
      Pi.topologicalSpace = TopologicalSpace.generateFrom {g : Set ((i : ι) → π i) | ∃ (s : (a : ι) → Set (π a)) (i : Finset ι), (∀ ai, IsOpen (s a)) g = (↑i).pi s}
      theorem pi_generateFrom_eq_finite {ι : Type u_5} {π : ιType u_9} {g : (a : ι) → Set (Set (π a))} [Finite ι] (hg : ∀ (a : ι), ⋃₀ g a = Set.univ) :
      Pi.topologicalSpace = TopologicalSpace.generateFrom {t : Set ((i : ι) → π i) | ∃ (s : (a : ι) → Set (π a)), (∀ (a : ι), s a g a) t = Set.univ.pi s}
      theorem induced_to_pi {ι : Type u_5} {π : ιType u_6} [T : (i : ι) → TopologicalSpace (π i)] {X : Type u_9} (f : X(i : ι) → π i) :
      TopologicalSpace.induced f Pi.topologicalSpace = ⨅ (i : ι), TopologicalSpace.induced (fun (x : X) => f x i) inferInstance
      theorem inducing_iInf_to_pi {ι : Type u_5} {π : ιType u_6} [T : (i : ι) → TopologicalSpace (π i)] {X : Type u_9} (f : (i : ι) → Xπ i) :
      Inducing fun (x : X) (i : ι) => f i x

      Suppose π i is a family of topological spaces indexed by i : ι, and X is a type endowed with a family of maps f i : X → π i for every i : ι, hence inducing a map g : X → Π i, π i. This lemma shows that infimum of the topologies on X induced by the f i as i : ι varies is simply the topology on X induced by g : X → Π i, π i where Π i, π i is endowed with the usual product topology.

      instance Pi.discreteTopology {ι : Type u_5} {π : ιType u_6} [T : (i : ι) → TopologicalSpace (π i)] [Finite ι] [∀ (i : ι), DiscreteTopology (π i)] :
      DiscreteTopology ((i : ι) → π i)

      A finite product of discrete spaces is discrete.

      Equations
      • =
      theorem continuous_sigmaMk {ι : Type u_5} {σ : ιType u_7} [(i : ι) → TopologicalSpace (σ i)] {i : ι} :
      theorem isOpen_sigma_iff {ι : Type u_5} {σ : ιType u_7} [(i : ι) → TopologicalSpace (σ i)] {s : Set (Sigma σ)} :
      IsOpen s ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
      theorem isClosed_sigma_iff {ι : Type u_5} {σ : ιType u_7} [(i : ι) → TopologicalSpace (σ i)] {s : Set (Sigma σ)} :
      IsClosed s ∀ (i : ι), IsClosed (Sigma.mk i ⁻¹' s)
      theorem isOpenMap_sigmaMk {ι : Type u_5} {σ : ιType u_7} [(i : ι) → TopologicalSpace (σ i)] {i : ι} :
      theorem isOpen_range_sigmaMk {ι : Type u_5} {σ : ιType u_7} [(i : ι) → TopologicalSpace (σ i)] {i : ι} :
      theorem isClosedMap_sigmaMk {ι : Type u_5} {σ : ιType u_7} [(i : ι) → TopologicalSpace (σ i)] {i : ι} :
      theorem isClosed_range_sigmaMk {ι : Type u_5} {σ : ιType u_7} [(i : ι) → TopologicalSpace (σ i)] {i : ι} :
      theorem openEmbedding_sigmaMk {ι : Type u_5} {σ : ιType u_7} [(i : ι) → TopologicalSpace (σ i)] {i : ι} :
      theorem closedEmbedding_sigmaMk {ι : Type u_5} {σ : ιType u_7} [(i : ι) → TopologicalSpace (σ i)] {i : ι} :
      theorem embedding_sigmaMk {ι : Type u_5} {σ : ιType u_7} [(i : ι) → TopologicalSpace (σ i)] {i : ι} :
      theorem Sigma.nhds_mk {ι : Type u_5} {σ : ιType u_7} [(i : ι) → TopologicalSpace (σ i)] (i : ι) (x : σ i) :
      nhds i, x = Filter.map (Sigma.mk i) (nhds x)
      theorem Sigma.nhds_eq {ι : Type u_5} {σ : ιType u_7} [(i : ι) → TopologicalSpace (σ i)] (x : Sigma σ) :
      nhds x = Filter.map (Sigma.mk x.fst) (nhds x.snd)
      theorem comap_sigmaMk_nhds {ι : Type u_5} {σ : ιType u_7} [(i : ι) → TopologicalSpace (σ i)] (i : ι) (x : σ i) :
      Filter.comap (Sigma.mk i) (nhds i, x) = nhds x
      theorem isOpen_sigma_fst_preimage {ι : Type u_5} {σ : ιType u_7} [(i : ι) → TopologicalSpace (σ i)] (s : Set ι) :
      IsOpen (Sigma.fst ⁻¹' s)
      @[simp]
      theorem continuous_sigma_iff {X : Type u} {ι : Type u_5} {σ : ιType u_7} [(i : ι) → TopologicalSpace (σ i)] [TopologicalSpace X] {f : Sigma σX} :
      Continuous f ∀ (i : ι), Continuous fun (a : σ i) => f i, a

      A map out of a sum type is continuous iff its restriction to each summand is.

      theorem continuous_sigma {X : Type u} {ι : Type u_5} {σ : ιType u_7} [(i : ι) → TopologicalSpace (σ i)] [TopologicalSpace X] {f : Sigma σX} (hf : ∀ (i : ι), Continuous fun (a : σ i) => f i, a) :

      A map out of a sum type is continuous if its restriction to each summand is.

      theorem inducing_sigma {X : Type u} {ι : Type u_5} {σ : ιType u_7} [(i : ι) → TopologicalSpace (σ i)] [TopologicalSpace X] {f : Sigma σX} :
      Inducing f (∀ (i : ι), Inducing (f Sigma.mk i)) ∀ (i : ι), ∃ (U : Set X), IsOpen U ∀ (x : Sigma σ), f x U x.fst = i

      A map defined on a sigma type (a.k.a. the disjoint union of an indexed family of topological spaces) is inducing iff its restriction to each component is inducing and each the image of each component under f can be separated from the images of all other components by an open set.

      @[simp]
      theorem continuous_sigma_map {ι : Type u_5} {κ : Type u_6} {σ : ιType u_7} {τ : κType u_8} [(i : ι) → TopologicalSpace (σ i)] [(k : κ) → TopologicalSpace (τ k)] {f₁ : ικ} {f₂ : (i : ι) → σ iτ (f₁ i)} :
      Continuous (Sigma.map f₁ f₂) ∀ (i : ι), Continuous (f₂ i)
      theorem Continuous.sigma_map {ι : Type u_5} {κ : Type u_6} {σ : ιType u_7} {τ : κType u_8} [(i : ι) → TopologicalSpace (σ i)] [(k : κ) → TopologicalSpace (τ k)] {f₁ : ικ} {f₂ : (i : ι) → σ iτ (f₁ i)} (hf : ∀ (i : ι), Continuous (f₂ i)) :
      Continuous (Sigma.map f₁ f₂)
      theorem isOpenMap_sigma {X : Type u} {ι : Type u_5} {σ : ιType u_7} [(i : ι) → TopologicalSpace (σ i)] [TopologicalSpace X] {f : Sigma σX} :
      IsOpenMap f ∀ (i : ι), IsOpenMap fun (a : σ i) => f i, a
      theorem isOpenMap_sigma_map {ι : Type u_5} {κ : Type u_6} {σ : ιType u_7} {τ : κType u_8} [(i : ι) → TopologicalSpace (σ i)] [(k : κ) → TopologicalSpace (τ k)] {f₁ : ικ} {f₂ : (i : ι) → σ iτ (f₁ i)} :
      IsOpenMap (Sigma.map f₁ f₂) ∀ (i : ι), IsOpenMap (f₂ i)
      theorem inducing_sigma_map {ι : Type u_5} {κ : Type u_6} {σ : ιType u_7} {τ : κType u_8} [(i : ι) → TopologicalSpace (σ i)] [(k : κ) → TopologicalSpace (τ k)] {f₁ : ικ} {f₂ : (i : ι) → σ iτ (f₁ i)} (h₁ : Function.Injective f₁) :
      Inducing (Sigma.map f₁ f₂) ∀ (i : ι), Inducing (f₂ i)
      theorem embedding_sigma_map {ι : Type u_5} {κ : Type u_6} {σ : ιType u_7} {τ : κType u_8} [(i : ι) → TopologicalSpace (σ i)] [(k : κ) → TopologicalSpace (τ k)] {f₁ : ικ} {f₂ : (i : ι) → σ iτ (f₁ i)} (h : Function.Injective f₁) :
      Embedding (Sigma.map f₁ f₂) ∀ (i : ι), Embedding (f₂ i)
      theorem openEmbedding_sigma_map {ι : Type u_5} {κ : Type u_6} {σ : ιType u_7} {τ : κType u_8} [(i : ι) → TopologicalSpace (σ i)] [(k : κ) → TopologicalSpace (τ k)] {f₁ : ικ} {f₂ : (i : ι) → σ iτ (f₁ i)} (h : Function.Injective f₁) :
      OpenEmbedding (Sigma.map f₁ f₂) ∀ (i : ι), OpenEmbedding (f₂ i)
      theorem ULift.isOpen_iff {X : Type u} [TopologicalSpace X] {s : Set (ULift.{v, u} X)} :
      IsOpen s IsOpen (ULift.up ⁻¹' s)
      theorem IsOpen.trans {X : Type u} [TopologicalSpace X] {s : Set X} {t : Set s} (ht : IsOpen t) (hs : IsOpen s) :
      IsOpen (Subtype.val '' t)
      theorem IsClosed.trans {X : Type u} [TopologicalSpace X] {s : Set X} {t : Set s} (ht : IsClosed t) (hs : IsClosed s) :
      IsClosed (Subtype.val '' t)
      theorem nhdsSet_prod_le {X : Type u_5} {Y : Type u_6} [TopologicalSpace X] [TopologicalSpace Y] (s : Set X) (t : Set Y) :

      The product of a neighborhood of s and a neighborhood of t is a neighborhood of s ×ˢ t, formulated in terms of a filter inequality.

      theorem Filter.eventually_nhdsSet_prod_iff {X : Type u_5} {Y : Type u_6} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {t : Set Y} {p : X × YProp} :
      (∀ᶠ (q : X × Y) in nhdsSet (s ×ˢ t), p q) xs, yt, ∃ (px : XProp), (∀ᶠ (x' : X) in nhds x, px x') ∃ (py : YProp), (∀ᶠ (y' : Y) in nhds y, py y') ∀ {x : X}, px x∀ {y : Y}, py yp (x, y)
      theorem Filter.Eventually.prod_nhdsSet {X : Type u_5} {Y : Type u_6} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {t : Set Y} {p : X × YProp} {px : XProp} {py : YProp} (hp : ∀ {x : X}, px x∀ {y : Y}, py yp (x, y)) (hs : ∀ᶠ (x : X) in nhdsSet s, px x) (ht : ∀ᶠ (y : Y) in nhdsSet t, py y) :
      ∀ᶠ (q : X × Y) in nhdsSet (s ×ˢ t), p q