# 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 : ] :
Equations
• instTopologicalSpaceQuot =
instance instTopologicalSpaceQuotient {X : Type u} {s : } [t : ] :
Equations
instance instTopologicalSpaceProd {X : Type u} {Y : Type v} [t₁ : ] [t₂ : ] :
Equations
instance instTopologicalSpaceSum {X : Type u} {Y : Type v} [t₁ : ] [t₂ : ] :
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
instance ULift.topologicalSpace {X : Type u} [t : ] :
Equations

### Additive, Multiplicative#

The topology on those type synonyms is inherited without change.

instance instTopologicalSpaceAdditive {X : Type u} [] :
Equations
Equations
• instTopologicalSpaceMultiplicative = inst
instance instDiscreteTopologyAdditive {X : Type u} [] [] :
Equations
• = inst
instance instDiscreteTopologyMultiplicative {X : Type u} [] [] :
Equations
• = inst
theorem continuous_ofMul {X : Type u} [] :
theorem continuous_toMul {X : Type u} [] :
theorem continuous_ofAdd {X : Type u} [] :
theorem continuous_toAdd {X : Type u} [] :
theorem isOpenMap_ofMul {X : Type u} [] :
theorem isOpenMap_toMul {X : Type u} [] :
theorem isOpenMap_ofAdd {X : Type u} [] :
theorem isOpenMap_toAdd {X : Type u} [] :
theorem isClosedMap_ofMul {X : Type u} [] :
theorem isClosedMap_toMul {X : Type u} [] :
theorem isClosedMap_ofAdd {X : Type u} [] :
theorem isClosedMap_toAdd {X : Type u} [] :
theorem nhds_ofMul {X : Type u} [] (x : X) :
theorem nhds_ofAdd {X : Type u} [] (x : X) :
theorem nhds_toMul {X : Type u} [] (x : ) :
theorem nhds_toAdd {X : Type u} [] (x : ) :

### Order dual #

The topology on this type synonym is inherited without change.

instance OrderDual.instTopologicalSpace {X : Type u} [] :
Equations
• OrderDual.instTopologicalSpace = inst
instance OrderDual.instDiscreteTopology {X : Type u} [] [] :
Equations
• = inst
theorem continuous_toDual {X : Type u} [] :
Continuous OrderDual.toDual
theorem continuous_ofDual {X : Type u} [] :
Continuous OrderDual.ofDual
theorem isOpenMap_toDual {X : Type u} [] :
IsOpenMap OrderDual.toDual
theorem isOpenMap_ofDual {X : Type u} [] :
IsOpenMap OrderDual.ofDual
theorem isClosedMap_toDual {X : Type u} [] :
IsClosedMap OrderDual.toDual
theorem isClosedMap_ofDual {X : Type u} [] :
IsClosedMap OrderDual.ofDual
theorem nhds_toDual {X : Type u} [] (x : X) :
nhds (OrderDual.toDual x) = Filter.map (OrderDual.toDual) (nhds x)
theorem nhds_ofDual {X : Type u} [] (x : X) :
nhds (OrderDual.ofDual x) = Filter.map (OrderDual.ofDual) (nhds x)
instance OrderDual.instNeBotNhdsWithinIoi {X : Type u} [] [] {x : X} [(nhdsWithin x ()).NeBot] :
(nhdsWithin (OrderDual.toDual x) (Set.Ioi (OrderDual.toDual x))).NeBot
Equations
• = inst
instance OrderDual.instNeBotNhdsWithinIio {X : Type u} [] [] {x : X} [(nhdsWithin x ()).NeBot] :
(nhdsWithin (OrderDual.toDual x) (Set.Iio (OrderDual.toDual x))).NeBot
Equations
• = inst
theorem Quotient.preimage_mem_nhds {X : Type u} [] [s : ] {V : Set ()} {x : X} (hs : V nhds ()) :
Quotient.mk' ⁻¹' V nhds x
theorem Dense.quotient {X : Type u} [] [] {s : Set X} (H : ) :
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} [] [] {f : YX} (hf : ) :
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} [] {s : } {t : } (h : s t) :
theorem continuous_map_sInf {α : Type u_5} [] {S : Set ()} {s : } (h : s S) :
instance instDiscreteTopologySubtype {X : Type u} {p : XProp} [] [] :
Equations
• =
instance Sum.discreteTopology {X : Type u} {Y : Type v} [] [] [h : ] [hY : ] :
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} [] (f : αβ) (y : β) :
theorem mem_nhds_subtype {X : Type u} [] (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} [] (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} [] (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} [] {s : Set X} {t : Set X} {x : s} :
nhdsWithin x (Subtype.val ⁻¹' t) = nhdsWithin (x) t =
theorem nhds_ne_subtype_eq_bot_iff {X : Type u} [] {S : Set X} {x : S} :
theorem nhds_ne_subtype_neBot_iff {X : Type u} [] {S : Set X} {x : S} :
(nhdsWithin x {x}).NeBot (nhdsWithin x {x} ).NeBot
theorem discreteTopology_subtype_iff {X : Type u} [] {S : Set X} :
xS, nhdsWithin x {x} =
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
• CofiniteTopology.of =
Instances For
instance CofiniteTopology.instInhabited {X : Type u} [] :
Equations
• CofiniteTopology.instInhabited = { default := CofiniteTopology.of default }
Equations
• CofiniteTopology.instTopologicalSpace = { IsOpen := fun (s : ) => s.Nonemptys.Finite, isOpen_univ := , isOpen_inter := , isOpen_sUnion := }
theorem CofiniteTopology.isOpen_iff {X : Type u} {s : } :
s.Nonemptys.Finite
theorem CofiniteTopology.isOpen_iff' {X : Type u} {s : } :
s = s.Finite
theorem CofiniteTopology.isClosed_iff {X : Type u} {s : } :
s = Set.univ s.Finite
theorem CofiniteTopology.nhds_eq {X : Type u} (x : ) :
nhds x = pure x Filter.cofinite
theorem CofiniteTopology.mem_nhds_iff {X : Type u} {x : } {s : } :
s nhds x x s s.Finite
@[simp]
theorem continuous_prod_mk {X : Type u} {Y : Type v} {Z : Type u_1} [] [] [] {f : XY} {g : XZ} :
(Continuous fun (x : X) => (f x, g x))
theorem continuous_fst {X : Type u} {Y : Type v} [] [] :
Continuous Prod.fst
theorem Continuous.fst {X : Type u} {Y : Type v} {Z : Type u_1} [] [] [] {f : XY × Z} (hf : ) :
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} [] [] [] {f : XZ} (hf : ) :
Continuous fun (x : X × Y) => f x.1

Precomposing f with Prod.fst is continuous

theorem continuousAt_fst {X : Type u} {Y : Type v} [] [] {p : X × Y} :
ContinuousAt Prod.fst p
theorem ContinuousAt.fst {X : Type u} {Y : Type v} {Z : Type u_1} [] [] [] {f : XY × Z} {x : X} (hf : ) :
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} [] [] [] {f : XZ} {x : X} {y : Y} (hf : ) :
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} [] [] [] {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} [] [] {X : Type u_5} {l : } {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} [] [] :
Continuous Prod.snd
theorem Continuous.snd {X : Type u} {Y : Type v} {Z : Type u_1} [] [] [] {f : XY × Z} (hf : ) :
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} [] [] [] {f : YZ} (hf : ) :
Continuous fun (x : X × Y) => f x.2

Precomposing f with Prod.snd is continuous

theorem continuousAt_snd {X : Type u} {Y : Type v} [] [] {p : X × Y} :
ContinuousAt Prod.snd p
theorem ContinuousAt.snd {X : Type u} {Y : Type v} {Z : Type u_1} [] [] [] {f : XY × Z} {x : X} (hf : ) :
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} [] [] [] {f : YZ} {x : X} {y : Y} (hf : ) :
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} [] [] [] {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} [] [] {X : Type u_5} {l : } {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} [] [] [] {f : ZX} {g : ZY} (hf : ) (hg : ) :
Continuous fun (x : Z) => (f x, g x)
theorem Continuous.Prod.mk {X : Type u} {Y : Type v} [] [] (x : X) :
Continuous fun (y : Y) => (x, y)
theorem Continuous.Prod.mk_left {X : Type u} {Y : Type v} [] [] (y : Y) :
Continuous fun (x : X) => (x, y)
theorem IsClosed.setOf_mapsTo {X : Type u} {Z : Type u_1} [] [] {α : Type u_5} {f : XαZ} {s : Set α} {t : Set Z} (ht : ) (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} [] [] [] [] {g : X × YZ} (hg : ) {e : WX} (he : ) {f : WY} (hf : ) :
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} [] [] [] [] [] {g : X × Y × Zε} (hg : ) {e : WX} (he : ) {f : WY} (hf : ) {k : WZ} (hk : ) :
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} [] [] [] [] [] [] {g : X × Y × Z × ζε} (hg : ) {e : WX} (he : ) {f : WY} (hf : ) {k : WZ} (hk : ) {l : Wζ} (hl : ) :
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} [] [] [] [] {f : ZX} {g : WY} (hf : ) (hg : ) :
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 : } {ta2 : } {tb1 : } {tb2 : } {tc1 : } (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 : } {ta2 : } {tb1 : } {tb2 : } {tc1 : } (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 : } {tbs : } {tX : } {tY : } {tc : } (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} [] [] {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} [] [] {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} [] [] {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} [] [] :
Continuous Prod.swap
theorem isClosedMap_swap {X : Type u} {Y : Type v} [] [] :
IsClosedMap Prod.swap
theorem Continuous.uncurry_left {X : Type u} {Y : Type v} {Z : Type u_1} [] [] [] {f : XYZ} (x : X) (h : ) :
theorem Continuous.uncurry_right {X : Type u} {Y : Type v} {Z : Type u_1} [] [] [] {f : XYZ} (y : Y) (h : ) :
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} [] [] [] {f : XYZ} (x : X) (h : ) :

Alias of Continuous.uncurry_left.

@[deprecated Continuous.uncurry_right]
theorem continuous_uncurry_right {X : Type u} {Y : Type v} {Z : Type u_1} [] [] [] {f : XYZ} (y : Y) (h : ) :
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} [] [] [] {g : X × YZ} (x : X) (h : ) :
theorem IsOpen.prod {X : Type u} {Y : Type v} [] [] {s : Set X} {t : Set Y} (hs : ) (ht : ) :
IsOpen (s ×ˢ t)
theorem nhds_prod_eq {X : Type u} {Y : Type v} [] [] {x : X} {y : Y} :
nhds (x, y) = nhds x ×ˢ nhds y
theorem nhdsWithin_prod_eq {X : Type u} {Y : Type v} [] [] (x : X) (y : Y) (s : Set X) (t : Set Y) :
nhdsWithin (x, y) (s ×ˢ t) = ×ˢ
instance Prod.instNeBotNhdsWithinIio {X : Type u} {Y : Type v} [] [] [] [] {x : X × Y} [hx₁ : (nhdsWithin x.1 (Set.Iio x.1)).NeBot] [hx₂ : (nhdsWithin x.2 (Set.Iio x.2)).NeBot] :
(nhdsWithin x ()).NeBot
Equations
• =
instance Prod.instNeBotNhdsWithinIoi {X : Type u} {Y : Type v} [] [] [] [] {x : X × Y} [(nhdsWithin x.1 (Set.Ioi x.1)).NeBot] [(nhdsWithin x.2 (Set.Ioi x.2)).NeBot] :
(nhdsWithin x ()).NeBot
Equations
• =
theorem mem_nhds_prod_iff {X : Type u} {Y : Type v} [] [] {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} [] [] {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} [] [] {ι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} [] [] {ι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 mem_nhds_prod_iff' {X : Type u} {Y : Type v} [] [] {x : X} {y : Y} {s : Set (X × Y)} :
s nhds (x, y) ∃ (u : Set X) (v : Set Y), x u y v u ×ˢ v s
theorem Prod.tendsto_iff {Y : Type v} {Z : Type u_1} [] [] {X : Type u_5} (seq : XY × Z) {f : } (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} [] [] [] [] :
Equations
• =
theorem prod_mem_nhds_iff {X : Type u} {Y : Type v} [] [] {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} [] [] {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} [] :
IsOpen {p : X × X | Disjoint (nhds p.1) (nhds p.2)}
theorem Filter.Eventually.prod_nhds {X : Type u} {Y : Type v} [] [] {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} [] [] (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} [] [] {γ : Type u_5} {x : X} {y : Y} {f : } {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} [] [] {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} [] [] [] {f : XY} {g : XZ} {x : X} (hf : ) (hg : ) :
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} [] [] [] [] {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} [] [] [] [] {f : XZ} {g : YW} {x : X} {y : Y} (hf : ) (hg : ) :
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} [] [] [] [] {f : Y × ZW} {g : XY} {h : XZ} {x : X} (hf : ContinuousAt f (g x, h x)) (hg : ) (hh : ) :
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} [] [] [] [] {f : Y × ZW} {g : XY} {h : XZ} {x : X} {y : Y × Z} (hf : ) (hg : ) (hh : ) (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} [] [] [] {f : X × YZ} (hf : ) {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} [] [] [] {f : X × YZ} (hf : ) {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} [] [] [] {f : X × YZ} (hf : ) {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} [] [] [] {f : X × YZ} (hf : ) {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 (x : Set X) (x_1 : Set Y) => x ×ˢ x_1) s t)
theorem prod_eq_generateFrom {X : Type u} {Y : Type v} [] [] :
instTopologicalSpaceProd = TopologicalSpace.generateFrom {g : Set (X × Y) | ∃ (s : Set X) (t : Set Y), g = s ×ˢ t}
theorem isOpen_prod_iff {X : Type u} {Y : Type v} [] [] {s : Set (X × Y)} :
∀ (a : X) (b : Y), (a, b) s∃ (u : Set X) (v : Set Y), a u b v u ×ˢ v s
theorem prod_induced_induced {Y : Type v} {W : Type u_2} [] [] {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} [] {s : Set (X × X)} {x : X} (hx : s nhds (x, x)) :
∃ (U : Set X), 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} [] [] (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} [] [] (x : X × Y) :
Filter.map Prod.fst (nhds x) = nhds x.1
theorem isOpenMap_fst {X : Type u} {Y : Type v} [] [] :
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} [] [] (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} [] [] (x : X × Y) :
Filter.map Prod.snd (nhds x) = nhds x.2
theorem isOpenMap_snd {X : Type u} {Y : Type v} [] [] :
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} [] [] {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} [] [] {s : Set X} {t : Set Y} :
theorem interior_prod_eq {X : Type u} {Y : Type v} [] [] (s : Set X) (t : Set Y) :
interior (s ×ˢ t) =
theorem frontier_prod_eq {X : Type u} {Y : Type v} [] [] (s : Set X) (t : Set Y) :
@[simp]
theorem frontier_prod_univ_eq {X : Type u} {Y : Type v} [] [] (s : Set X) :
frontier (s ×ˢ Set.univ) = ×ˢ Set.univ
@[simp]
theorem frontier_univ_prod_eq {X : Type u} {Y : Type v} [] [] (s : Set Y) :
frontier (Set.univ ×ˢ s) = Set.univ ×ˢ
theorem map_mem_closure₂ {X : Type u} {Y : Type v} {Z : Type u_1} [] [] [] {f : XYZ} {x : X} {y : Y} {s : Set X} {t : Set Y} {u : Set Z} (hf : ) (hx : x ) (hy : y ) (h : as, bt, f a b u) :
f x y
theorem IsClosed.prod {X : Type u} {Y : Type v} [] [] {s₁ : Set X} {s₂ : Set Y} (h₁ : IsClosed s₁) (h₂ : IsClosed s₂) :
IsClosed (s₁ ×ˢ s₂)
theorem Dense.prod {X : Type u} {Y : Type v} [] [] {s : Set X} {t : Set Y} (hs : ) (ht : ) :
Dense (s ×ˢ t)

The product of two dense sets is a dense set.

theorem DenseRange.prod_map {Y : Type v} {Z : Type u_1} [] [] {ι : Type u_5} {κ : Type u_6} {f : ιY} {g : κZ} (hf : ) (hg : ) :

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} [] [] [] [] {f : XY} {g : ZW} (hf : ) (hg : ) :
@[simp]
theorem inducing_const_prod {X : Type u} {Y : Type v} {Z : Type u_1} [] [] [] {x : X} {f : YZ} :
(Inducing fun (x' : Y) => (x, f x'))
@[simp]
theorem inducing_prod_const {X : Type u} {Y : Type v} {Z : Type u_1} [] [] [] {y : Y} {f : XZ} :
(Inducing fun (x : X) => (f x, y))
theorem Embedding.prod_map {X : Type u} {Y : Type v} {Z : Type u_1} {W : Type u_2} [] [] [] [] {f : XY} {g : ZW} (hf : ) (hg : ) :
theorem IsOpenMap.prod {X : Type u} {Y : Type v} {Z : Type u_1} {W : Type u_2} [] [] [] [] {f : XY} {g : ZW} (hf : ) (hg : ) :
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} [] [] [] [] {f : XY} {g : ZW} (hf : ) (hg : ) :
OpenEmbedding fun (x : X × Z) => (f x.1, g x.2)
theorem embedding_graph {X : Type u} {Y : Type v} [] [] {f : XY} (hf : ) :
Embedding fun (x : X) => (x, f x)
theorem embedding_prod_mk {X : Type u} {Y : Type v} [] [] (x : X) :
theorem continuous_bool_rng {X : Type u} [] {f : XBool} (b : Bool) :
theorem continuous_sum_dom {X : Type u} {Y : Type v} {Z : Type u_1} [] [] [] {f : X YZ} :
Continuous (f Sum.inl) Continuous (f Sum.inr)
theorem continuous_sum_elim {X : Type u} {Y : Type v} {Z : Type u_1} [] [] [] {f : XZ} {g : YZ} :
theorem Continuous.sum_elim {X : Type u} {Y : Type v} {Z : Type u_1} [] [] [] {f : XZ} {g : YZ} (hf : ) (hg : ) :
theorem continuous_isLeft {X : Type u} {Y : Type v} [] [] :
Continuous Sum.isLeft
theorem continuous_isRight {X : Type u} {Y : Type v} [] [] :
Continuous Sum.isRight
theorem continuous_inl {X : Type u} {Y : Type v} [] [] :
Continuous Sum.inl
theorem continuous_inr {X : Type u} {Y : Type v} [] [] :
Continuous Sum.inr
theorem isOpen_sum_iff {X : Type u} {Y : Type v} [] [] {s : Set (X Y)} :
IsOpen (Sum.inl ⁻¹' s) IsOpen (Sum.inr ⁻¹' s)
theorem isClosed_sum_iff {X : Type u} {Y : Type v} [] [] {s : Set (X Y)} :
IsClosed (Sum.inl ⁻¹' s) IsClosed (Sum.inr ⁻¹' s)
theorem isOpenMap_inl {X : Type u} {Y : Type v} [] [] :
IsOpenMap Sum.inl
theorem isOpenMap_inr {X : Type u} {Y : Type v} [] [] :
IsOpenMap Sum.inr
theorem openEmbedding_inl {X : Type u} {Y : Type v} [] [] :
theorem openEmbedding_inr {X : Type u} {Y : Type v} [] [] :
theorem embedding_inl {X : Type u} {Y : Type v} [] [] :
Embedding Sum.inl
theorem embedding_inr {X : Type u} {Y : Type v} [] [] :
Embedding Sum.inr
theorem isOpen_range_inl {X : Type u} {Y : Type v} [] [] :
IsOpen (Set.range Sum.inl)
theorem isOpen_range_inr {X : Type u} {Y : Type v} [] [] :
IsOpen (Set.range Sum.inr)
theorem isClosed_range_inl {X : Type u} {Y : Type v} [] [] :
theorem isClosed_range_inr {X : Type u} {Y : Type v} [] [] :
theorem closedEmbedding_inl {X : Type u} {Y : Type v} [] [] :
theorem closedEmbedding_inr {X : Type u} {Y : Type v} [] [] :
theorem nhds_inl {X : Type u} {Y : Type v} [] [] (x : X) :
nhds () = Filter.map Sum.inl (nhds x)
theorem nhds_inr {X : Type u} {Y : Type v} [] [] (y : Y) :
nhds () = 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} [] [] [] [] {f : XY} {g : ZW} :
theorem Continuous.sum_map {X : Type u} {Y : Type v} {Z : Type u_1} {W : Type u_2} [] [] [] [] {f : XY} {g : ZW} (hf : ) (hg : ) :
theorem isOpenMap_sum {X : Type u} {Y : Type v} {Z : Type u_1} [] [] [] {f : X YZ} :
(IsOpenMap fun (a : X) => f ()) IsOpenMap fun (b : Y) => f ()
@[simp]
theorem isOpenMap_sum_elim {X : Type u} {Y : Type v} {Z : Type u_1} [] [] [] {f : XZ} {g : YZ} :
theorem IsOpenMap.sum_elim {X : Type u} {Y : Type v} {Z : Type u_1} [] [] [] {f : XZ} {g : YZ} (hf : ) (hg : ) :
theorem isClosedMap_sum {X : Type u} {Y : Type v} {Z : Type u_1} [] [] [] {f : X YZ} :
(IsClosedMap fun (a : X) => f ()) IsClosedMap fun (b : Y) => f ()
theorem inducing_subtype_val {Y : Type v} [] {t : Set Y} :
Inducing Subtype.val
theorem Inducing.of_codRestrict {X : Type u} {Y : Type v} [] [] {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} [] {p : XProp} :
Embedding Subtype.val
theorem closedEmbedding_subtype_val {X : Type u} [] {p : XProp} (h : IsClosed {a : X | p a}) :
ClosedEmbedding Subtype.val
theorem continuous_subtype_val {X : Type u} [] {p : XProp} :
Continuous Subtype.val
theorem Continuous.subtype_val {X : Type u} {Y : Type v} [] [] {p : XProp} {f : Y} (hf : ) :
Continuous fun (x : Y) => (f x)
theorem IsOpen.openEmbedding_subtype_val {X : Type u} [] {s : Set X} (hs : ) :
OpenEmbedding Subtype.val
theorem IsOpen.isOpenMap_subtype_val {X : Type u} [] {s : Set X} (hs : ) :
IsOpenMap Subtype.val
theorem IsOpenMap.restrict {X : Type u} {Y : Type v} [] [] {f : XY} (hf : ) {s : Set X} (hs : ) :
IsOpenMap (s.restrict f)
theorem IsClosed.closedEmbedding_subtype_val {X : Type u} [] {s : Set X} (hs : ) :
ClosedEmbedding Subtype.val
theorem IsClosed.isClosedMap_subtype_val {X : Type u} [] {s : Set X} (hs : ) :
IsClosedMap Subtype.val
theorem Continuous.subtype_mk {X : Type u} {Y : Type v} [] [] {p : XProp} {f : YX} (h : ) (hp : ∀ (x : Y), p (f x)) :
Continuous fun (x : Y) => f x,
theorem Continuous.subtype_map {X : Type u} {Y : Type v} [] [] {p : XProp} {f : XY} (h : ) {q : YProp} (hpq : ∀ (x : X), p xq (f x)) :
theorem continuous_inclusion {X : Type u} [] {s : Set X} {t : Set X} (h : s t) :
theorem continuousAt_subtype_val {X : Type u} [] {p : XProp} {x : } :
ContinuousAt Subtype.val x
theorem Subtype.dense_iff {X : Type u} [] {s : Set X} {t : Set s} :
s closure (Subtype.val '' t)
theorem map_nhds_subtype_val {X : Type u} [] {s : Set X} (x : s) :
Filter.map Subtype.val (nhds x) = nhdsWithin (x) s
theorem map_nhds_subtype_coe_eq_nhds {X : Type u} [] {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} [] {p : XProp} {x : X} {h : p x} :
nhds x, h = Filter.comap Subtype.val (nhds x)
theorem tendsto_subtype_rng {X : Type u} [] {Y : Type u_5} {p : XProp} {l : } {f : Y} {x : } :
Filter.Tendsto f l (nhds x) Filter.Tendsto (fun (x : Y) => (f x)) l (nhds x)
theorem closure_subtype {X : Type u} [] {p : XProp} {x : { a : X // p a }} {s : Set { a : X // p a }} :
x x closure (Subtype.val '' s)
@[simp]
theorem continuousAt_codRestrict_iff {X : Type u} {Y : Type v} [] [] {f : XY} {t : Set Y} (h1 : ∀ (x : X), f x t) {x : X} :
theorem ContinuousAt.codRestrict {X : Type u} {Y : Type v} [] [] {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} [] [] {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} [] [] {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} [] [] {f : XY} {s : Set Y} (hf : ) (hs : ∀ (a : X), f a s) :
theorem Continuous.restrict {X : Type u} {Y : Type v} [] [] {f : XY} {s : Set X} {t : Set Y} (h1 : Set.MapsTo f s t) (h2 : ) :
theorem Continuous.restrictPreimage {X : Type u} {Y : Type v} [] [] {f : XY} {s : Set Y} (h : ) :
Continuous (s.restrictPreimage f)
theorem Inducing.codRestrict {X : Type u} {Y : Type v} [] [] {e : XY} (he : ) {s : Set Y} (hs : ∀ (x : X), e x s) :
theorem Embedding.codRestrict {X : Type u} {Y : Type v} [] [] {e : XY} (he : ) (s : Set Y) (hs : ∀ (x : X), e x s) :
theorem embedding_inclusion {X : Type u} [] {s : Set X} {t : Set X} (h : s t) :
theorem DiscreteTopology.of_subset {X : Type u_5} [] {s : Set X} {t : Set X} :
t s

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.

theorem DiscreteTopology.preimage_of_continuous_injective {X : Type u_5} {Y : Type u_6} [] [] (s : Set Y) [] {f : XY} (hc : ) (hinj : ) :

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} [] [] {f : XY} (hf : ) {s : Set Y} (hs : ) :
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} [] {s : Set X} {t : Set X} :
IsClosed (Subtype.val ⁻¹' t) s closure (s t) t
theorem quotientMap_quot_mk {X : Type u} [] {r : XXProp} :
theorem continuous_quot_mk {X : Type u} [] {r : XXProp} :
theorem continuous_quot_lift {X : Type u} {Y : Type v} [] [] {r : XXProp} {f : XY} (hr : ∀ (a b : X), r a bf a = f b) (h : ) :
theorem quotientMap_quotient_mk' {X : Type u} [] {s : } :
QuotientMap Quotient.mk'
theorem continuous_quotient_mk' {X : Type u} [] {s : } :
Continuous Quotient.mk'
theorem Continuous.quotient_lift {X : Type u} {Y : Type v} [] [] {s : } {f : XY} (h : ) (hs : ∀ (a b : X), a bf a = f b) :
theorem Continuous.quotient_liftOn' {X : Type u} {Y : Type v} [] [] {s : } {f : XY} (h : ) (hs : ∀ (a b : X), Setoid.r a bf a = f b) :
Continuous fun (x : ) => x.liftOn' f hs
theorem Continuous.quotient_map' {X : Type u} {Y : Type v} [] [] {s : } {t : } {f : XY} (hf : ) (H : (Setoid.r Setoid.r) f f) :
theorem continuous_pi_iff {X : Type u} {ι : Type u_5} {π : ιType u_6} [] [T : (i : ι) → TopologicalSpace (π i)] {f : X(i : ι) → π i} :
∀ (i : ι), Continuous fun (a : X) => f a i
theorem continuous_pi {X : Type u} {ι : Type u_5} {π : ιType u_6} [] [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 : } {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.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} [] [T : (i : ι) → TopologicalSpace (π i)] {f : X(i : ι) → π i} {x : X} :
∀ (i : ι), ContinuousAt (fun (y : X) => f y i) x
theorem continuousAt_pi' {X : Type u} {ι : Type u_5} {π : ιType u_6} [] [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} [] {ι' : 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} [] [] {g : XY} (hg : ) :
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} [] {ι' : 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.induced_restrict {ι : Type u_5} {π : ιType u_6} [T : (i : ι) → TopologicalSpace (π i)] (S : Set ι) :
TopologicalSpace.induced S.restrict Pi.topologicalSpace = iS,
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)] [] {l : } {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} [] [T : (i : ι) → TopologicalSpace (π i)] {f : X(i : ι) → π i} [] {x : X} (hf : ) (i : ι) {g : Xπ i} (hg : ) :
ContinuousAt (fun (a : X) => Function.update (f a) i (g a)) x
theorem Continuous.update {X : Type u} {ι : Type u_5} {π : ιType u_6} [] [T : (i : ι) → TopologicalSpace (π i)] {f : X(i : ι) → π i} [] (hf : ) (i : ι) {g : Xπ i} (hg : ) :
Continuous fun (a : X) => Function.update (f a) i (g a)
theorem continuous_update {ι : Type u_5} {π : ιType u_6} [T : (i : ι) → TopologicalSpace (π i)] [] (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)] [] (i : ι) :
Continuous fun (x : π i) =>

Pi.single i x is continuous in x.

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

Pi.mulSingle i x is continuous in x.

theorem Filter.Tendsto.fin_insertNth {Y : Type v} {n : } {π : Fin (n + 1)Type u_8} [(i : Fin (n + 1)) → TopologicalSpace (π i)] (i : Fin (n + 1)) {f : Yπ i} {l : } {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} [] {n : } {π : Fin (n + 1)Type u_8} [(i : Fin (n + 1)) → TopologicalSpace (π i)] (i : Fin (n + 1)) {f : Xπ i} {x : X} (hf : ) {g : X(j : Fin n) → π (i.succAbove j)} (hg : ) :
ContinuousAt (fun (a : X) => i.insertNth (f a) (g a)) x
theorem Continuous.fin_insertNth {X : Type u} [] {n : } {π : Fin (n + 1)Type u_8} [(i : Fin (n + 1)) → TopologicalSpace (π i)] (i : Fin (n + 1)) {f : Xπ i} (hf : ) {g : X(j : Fin n) → π (i.succAbove j)} (hg : ) :
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)} :
fs, ∃ (I : ) (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)] [] {s : Set ((a : ι) → π a)} :
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)] [] {s : Set ((a : ι) → π a)} {x : (a : ι) → π a} (hs : s nhds x) (y : (a : ι) → π a) :
∃ (I : ), I.piecewise x y s
theorem pi_generateFrom_eq {ι : Type u_5} {π : ιType u_8} {g : (a : ι) → Set (Set (π a))} :
Pi.topologicalSpace = TopologicalSpace.generateFrom {t : Set ((i : ι) → π i) | ∃ (s : (a : ι) → Set (π a)) (i : ), (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 : ), (ai, IsOpen (s a)) g = (i).pi s}
theorem pi_generateFrom_eq_finite {ι : Type u_5} {π : ιType u_8} {g : (a : ι) → Set (Set (π a))} [] (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_8} (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_8} (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)] [] [∀ (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 ()} :
∀ (i : ι), IsOpen ( ⁻¹' s)
theorem isClosed_sigma_iff {ι : Type u_5} {σ : ιType u_7} [(i : ι) → TopologicalSpace (σ i)] {s : Set ()} :
∀ (i : ι), IsClosed ( ⁻¹' 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 () (nhds x)
theorem Sigma.nhds_eq {ι : Type u_5} {σ : ιType u_7} [(i : ι) → TopologicalSpace (σ i)] (x : ) :
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 () (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)] [] {f : X} :
∀ (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)] [] {f : 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)] [] {f : X} :
(∀ (i : ι), Inducing (f )) ∀ (i : ι), ∃ (U : Set X), ∀ (x : ), 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)] [] {f : X} :
∀ (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₁ : ) :
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 : ) :
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 : ) :
OpenEmbedding (Sigma.map f₁ f₂) ∀ (i : ι), OpenEmbedding (f₂ i)
theorem ULift.isOpen_iff {X : Type u} [] {s : Set ()} :
IsOpen (ULift.up ⁻¹' s)
theorem ULift.isClosed_iff {X : Type u} [] {s : Set ()} :
IsClosed (ULift.up ⁻¹' s)
theorem continuous_uLift_down {X : Type u} [] :
Continuous ULift.down
theorem continuous_uLift_up {X : Type u} [] :
Continuous ULift.up
theorem embedding_uLift_down {X : Type u} [] :
Embedding ULift.down
instance instDiscreteTopologyULift {X : Type u} [] [] :
Equations
• =
theorem IsOpen.trans {X : Type u} [] {s : Set X} {t : Set s} (ht : ) (hs : ) :
IsOpen (Subtype.val '' t)
theorem IsClosed.trans {X : Type u} [] {s : Set X} {t : Set s} (ht : ) (hs : ) :
IsClosed (Subtype.val '' t)
theorem nhdsSet_prod_le {X : Type u_5} {Y : Type u_6} [] [] (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} [] [] {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} [] [] {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 , px x) (ht : ∀ᶠ (y : Y) in , py y) :
∀ᶠ (q : X × Y) in nhdsSet (s ×ˢ t), p q