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 : X → X → Prop} [t : TopologicalSpace X] : TopologicalSpace (Quot r)

Equations

• instTopologicalSpaceQuot = TopologicalSpace.coinduced (Quot.mk r) t

instance instTopologicalSpaceQuotient {X : Type u} {s : Setoid X} [t : TopologicalSpace X] : TopologicalSpace (Quotient s)

Equations

• instTopologicalSpaceQuotient = TopologicalSpace.coinduced Quotient.mk' t

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

Equations

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

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

Equations

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

instance instTopologicalSpaceSigma {ι : Type u_5} {X : ι → Type v} [t₂ : (i : ι) → TopologicalSpace (X i)] : TopologicalSpace (Sigma X)

Equations

• instTopologicalSpaceSigma = ⨆ (i : ι), TopologicalSpace.coinduced (Sigma.mk i) (t₂ i)

instance Pi.topologicalSpace {ι : Type u_5} {Y : ι → Type v} [t₂ : (i : ι) → TopologicalSpace (Y i)] : TopologicalSpace ((i : ι) → Y i)

Equations

• Pi.topologicalSpace = ⨅ (i : ι), TopologicalSpace.induced (fun (f : (i : ι) → Y i) => f i) (t₂ i)

instance ULift.topologicalSpace {X : Type u} [t : TopologicalSpace X] : TopologicalSpace (ULift.{v, u} X)

Equations

• ULift.topologicalSpace = TopologicalSpace.induced ULift.down t

Additive, Multiplicative

The topology on those type synonyms is inherited without change.

instance instTopologicalSpaceAdditive {X : Type u} [TopologicalSpace X] : TopologicalSpace (Additive X)

Equations

• instTopologicalSpaceAdditive = inst

instance instTopologicalSpaceMultiplicative {X : Type u} [TopologicalSpace X] : TopologicalSpace (Multiplicative X)

Equations

• instTopologicalSpaceMultiplicative = inst

instance instDiscreteTopologyAdditive {X : Type u} [TopologicalSpace X] [DiscreteTopology X] : DiscreteTopology (Additive X)

Equations

• ⋯ = inst

instance instDiscreteTopologyMultiplicative {X : Type u} [TopologicalSpace X] [DiscreteTopology X] : DiscreteTopology (Multiplicative X)

Equations

• ⋯ = 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.

instance OrderDual.instTopologicalSpace {X : Type u} [TopologicalSpace X] : TopologicalSpace Xᵒᵈ

Equations

• OrderDual.instTopologicalSpace = inst

instance OrderDual.instDiscreteTopology {X : Type u} [TopologicalSpace X] [DiscreteTopology X] : DiscreteTopology Xᵒᵈ

Equations

• ⋯ = 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 : Y → X} (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) : Continuous (Setoid.map_of_le h)

theorem continuous_map_sInf {α : Type u_5} [TopologicalSpace α] {S : Set (Setoid α)} {s : Setoid α} (h : s ∈ S) : Continuous (Setoid.map_sInf h)

instance instDiscreteTopologySubtype {X : Type u} {p : X → Prop} [TopologicalSpace X] [DiscreteTopology X] : DiscreteTopology (Subtype p)

Equations

• ⋯ = ⋯

instance Sum.discreteTopology {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [h : DiscreteTopology X] [hY : DiscreteTopology Y] : DiscreteTopology (X ⊕ Y)

Equations

• ⋯ = ⋯

instance Sigma.discreteTopology {ι : Type u_5} {Y : ι → Type v} [(i : ι) → TopologicalSpace (Y i)] [h : ∀ (i : ι), DiscreteTopology (Y i)] : DiscreteTopology (Sigma Y)

Equations

• ⋯ = ⋯

@[simp]

theorem comap_nhdsWithin_range {α : Type u_5} {β : Type u_6} [TopologicalSpace β] (f : α → β) (y : β) : Filter.comap f (nhdsWithin y (Set.range f)) = Filter.comap f (nhds 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 ↔ ∃ u ∈ nhds ↑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_eq_bot_iff {X : Type u} [TopologicalSpace X] {S : Set X} {x : ↑S} : nhdsWithin x {x}ᶜ = ⊥ ↔ nhdsWithin ↑x {↑x}ᶜ ⊓ 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

theorem discreteTopology_subtype_iff {X : Type u} [TopologicalSpace X] {S : Set X} : DiscreteTopology ↑S ↔ ∀ x ∈ S, nhdsWithin x {x}ᶜ ⊓ Filter.principal S = ⊥

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

• CofiniteTopology X = X

def CofiniteTopology.of {X : Type u} : X ≃ CofiniteTopology X

The identity equivalence between `` and CofiniteTopology .

Equations

• CofiniteTopology.of = Equiv.refl X

instance CofiniteTopology.instInhabited {X : Type u} [Inhabited X] : Inhabited (CofiniteTopology X)

Equations

• CofiniteTopology.instInhabited = { default := CofiniteTopology.of default }

instance CofiniteTopology.instTopologicalSpace {X : Type u} : TopologicalSpace (CofiniteTopology X)

Equations

• CofiniteTopology.instTopologicalSpace = { IsOpen := fun (s : Set (CofiniteTopology X)) => s.Nonempty → sᶜ.Finite, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }

theorem CofiniteTopology.isOpen_iff {X : Type u} {s : Set (CofiniteTopology X)} : IsOpen s ↔ s.Nonempty → sᶜ.Finite

theorem CofiniteTopology.isOpen_iff' {X : Type u} {s : Set (CofiniteTopology X)} : IsOpen s ↔ s = ∅ ∨ sᶜ.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

theorem CofiniteTopology.mem_nhds_iff {X : Type u} {x : CofiniteTopology X} {s : Set (CofiniteTopology X)} : s ∈ nhds x ↔ x ∈ s ∧ sᶜ.Finite

@[simp]

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

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

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

Postcomposing f with Prod.fst is continuous

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

Precomposing f with Prod.fst is continuous

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

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

Postcomposing f with Prod.fst is continuous at x

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

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

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

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

theorem Filter.Tendsto.fst_nhds {Y : Type v} {Z : Type u_1} [TopologicalSpace Y] [TopologicalSpace Z] {X : Type u_5} {l : Filter X} {f : X → Y × 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 : X → Y × Z} (hf : Continuous f) : Continuous fun (x : X) => (f x).2

Postcomposing f with Prod.snd is continuous

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

Precomposing f with Prod.snd is continuous

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

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

Postcomposing f with Prod.snd is continuous at x

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

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

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

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

theorem Filter.Tendsto.snd_nhds {Y : Type v} {Z : Type u_1} [TopologicalSpace Y] [TopologicalSpace Z] {X : Type u_5} {l : Filter X} {f : X → Y × 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 : Z → X} {g : Z → Y} (hf : Continuous f) (hg : Continuous g) : Continuous fun (x : Z) => (f x, g x)

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

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

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

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

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

theorem Continuous.comp₃ {X : Type u} {Y : Type v} {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 : W → X} (he : Continuous e) {f : W → Y} (hf : Continuous f) {k : W → Z} (hk : Continuous k) : Continuous fun (w : W) => g (e w, f w, k w)

theorem Continuous.comp₄ {X : Type u} {Y : Type v} {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 : W → X} (he : Continuous e) {f : W → Y} (hf : Continuous f) {k : W → Z} (hk : Continuous k) {l : W → ζ} (hl : Continuous l) : Continuous fun (w : W) => g (e w, f w, k w, l w)

theorem Continuous.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 : Z → X} {g : W → Y} (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 : X → Y → Z} {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 : X → Y → Z} {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 : X → Y → Z} {tas : Set (TopologicalSpace X)} {tbs : Set (TopologicalSpace Y)} {tX : TopologicalSpace X} {tY : TopologicalSpace Y} {tc : TopologicalSpace Z} (hX : tX ∈ tas) (hY : tY ∈ tbs) (hf : Continuous fun (p : X × Y) => f p.1 p.2) : Continuous fun (p : X × Y) => f p.1 p.2

A version of continuous_sInf_dom for binary functions

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

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

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

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

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

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

theorem Continuous.uncurry_right {X : Type u} {Y : Type v} {Z : Type u_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y → Z} (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 : X → Y → Z} (x : X) (h : Continuous (Function.uncurry f)) : Continuous (f x)

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 : X → Y → Z} (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 × Y → Z} (x : X) (h : Continuous g) : Continuous (Function.curry g x)

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

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

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

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

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) ↔ ∃ u ∈ nhds x, ∃ v ∈ nhds y, u ×ˢ v ⊆ s

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

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

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

theorem 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 : X → Y × Z) {f : Filter X} (p : Y × Z) : Filter.Tendsto seq f (nhds p) ↔ Filter.Tendsto (fun (n : X) => (seq n).1) f (nhds p.1) ∧ Filter.Tendsto (fun (n : X) => (seq n).2) f (nhds p.2)

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

Equations

• ⋯ = ⋯

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

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

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

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

theorem 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 × Y → Prop} {x : X} {y : Y} (h : ∀ᶠ (x : X × Y) in nhds (x, y), p x) : ∀ᶠ (x' : X) in nhds x, ∀ᶠ (y' : Y) in nhds y, p (x', y')

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

theorem ContinuousAt.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 : X → Z} {g : Y → W} {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 : X → Z} {g : Y → W} {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 × Z → W} {g : X → Y} {h : X → Z} {x : X} (hf : ContinuousAt f (g x, h x)) (hg : ContinuousAt g x) (hh : ContinuousAt h x) : ContinuousAt (fun (x : X) => f (g x, h x)) x

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

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

Continuous functions on products are continuous in their first argument

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

Alias of Continuous.curry_left.

---

Continuous functions on products are continuous in their first argument

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

Continuous functions on products are continuous in their second argument

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

Alias of Continuous.curry_right.

---

Continuous functions on products are continuous in their second argument

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

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

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

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

A product of induced topologies is induced by the product map

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

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

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

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

@[simp]

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

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

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

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

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

@[simp]

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

The product of two dense sets is a dense set.

theorem DenseRange.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) : DenseRange (Prod.map f 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 : X → Y} {g : Z → W} (hf : Inducing f) (hg : Inducing g) : Inducing (Prod.map f 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 : Y → Z} : (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 : X → Z} : (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 : X → Y} {g : Z → W} (hf : Embedding f) (hg : Embedding g) : Embedding (Prod.map f 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 : X → Y} {g : Z → W} (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 : X → Y} {g : Z → W} (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 : X → Y} (hf : Continuous f) : Embedding fun (x : X) => (x, f x)

theorem embedding_prod_mk {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (x : X) : Embedding (Prod.mk 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 : X → Y} {g : Z → W} (hf : IsOpenQuotientMap f) (hg : IsOpenQuotientMap g) : IsOpenQuotientMap (Prod.map f g)

theorem continuous_bool_rng {X : Type u} [TopologicalSpace X] {f : X → Bool} (b : Bool) : Continuous f ↔ IsClopen (f ⁻¹' {b})

theorem continuous_sum_dom {X : Type u} {Y : Type v} {Z : Type u_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X ⊕ Y → Z} : 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 : X → Z} {g : Y → Z} : Continuous (Sum.elim f g) ↔ Continuous f ∧ Continuous g

theorem Continuous.sum_elim {X : Type u} {Y : Type v} {Z : Type u_1} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Z} {g : Y → Z} (hf : Continuous f) (hg : Continuous g) : Continuous (Sum.elim f 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 continuous_inl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : Continuous Sum.inl

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

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

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

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

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

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

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

theorem openEmbedding_inr {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : OpenEmbedding 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 isOpen_range_inl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : IsOpen (Set.range Sum.inl)

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

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

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

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

theorem closedEmbedding_inr {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : ClosedEmbedding 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 : X → Y} {g : Z → W} : Continuous (Sum.map f g) ↔ Continuous f ∧ Continuous g

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 : X → Y} {g : Z → W} (hf : Continuous f) (hg : Continuous g) : Continuous (Sum.map f g)

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

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

@[simp]

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

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

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

theorem 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 : X → Y} {t : Set Y} (ht : ∀ (x : X), f x ∈ t) (h : Inducing (Set.codRestrict f t ht)) : Inducing f

theorem embedding_subtype_val {X : Type u} [TopologicalSpace X] {p : X → Prop} : Embedding Subtype.val

theorem closedEmbedding_subtype_val {X : Type u} [TopologicalSpace X] {p : X → Prop} (h : IsClosed {a : X | p a}) : ClosedEmbedding Subtype.val

theorem continuous_subtype_val {X : Type u} [TopologicalSpace X] {p : X → Prop} : Continuous Subtype.val

theorem Continuous.subtype_val {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {p : X → Prop} {f : Y → Subtype 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 : X → Y} (hf : IsOpenMap f) {s : Set X} (hs : IsOpen s) : IsOpenMap (s.restrict f)

theorem IsClosed.closedEmbedding_subtype_val {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsClosed s) : ClosedEmbedding Subtype.val

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 : X → Prop} {f : Y → X} (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 : X → Prop} {f : X → Y} (h : Continuous f) {q : Y → Prop} (hpq : ∀ (x : X), p x → q (f x)) : Continuous (Subtype.map f hpq)

theorem continuous_inclusion {X : Type u} [TopologicalSpace X] {s : Set X} {t : Set X} (h : s ⊆ t) : Continuous (Set.inclusion h)

theorem continuousAt_subtype_val {X : Type u} [TopologicalSpace X] {p : X → Prop} {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 : X → Prop} {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 : X → Prop} {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 : X → Prop} {l : Filter Y} {f : Y → Subtype 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 : X → Prop} {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 : X → Y} {t : Set Y} (h1 : ∀ (x : X), f x ∈ t) {x : X} : ContinuousAt (Set.codRestrict f t h1) x ↔ ContinuousAt f x

theorem ContinuousAt.codRestrict {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {t : Set Y} (h1 : ∀ (x : X), f x ∈ t) {x : X} : ContinuousAt f x → ContinuousAt (Set.codRestrict f t h1) x

Alias of the reverse direction of continuousAt_codRestrict_iff.

theorem ContinuousAt.restrict {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} {t : Set Y} (h1 : Set.MapsTo f s t) {x : ↑s} (h2 : ContinuousAt f ↑x) : ContinuousAt (Set.MapsTo.restrict f s t h1) x

theorem ContinuousAt.restrictPreimage {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {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 : X → Y} {s : Set Y} (hf : Continuous f) (hs : ∀ (a : X), f a ∈ s) : Continuous (Set.codRestrict f s hs)

theorem Continuous.restrict {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} {t : Set Y} (h1 : Set.MapsTo f s t) (h2 : Continuous f) : Continuous (Set.MapsTo.restrict f s t h1)

theorem Continuous.restrictPreimage {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set Y} (h : Continuous f) : Continuous (s.restrictPreimage f)

theorem Inducing.codRestrict {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {e : X → Y} (he : Inducing e) {s : Set Y} (hs : ∀ (x : X), e x ∈ s) : Inducing (Set.codRestrict e s hs)

theorem Embedding.codRestrict {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {e : X → Y} (he : Embedding e) (s : Set Y) (hs : ∀ (x : X), e x ∈ s) : Embedding (Set.codRestrict e s hs)

theorem embedding_inclusion {X : Type u} [TopologicalSpace X] {s : Set X} {t : Set X} (h : s ⊆ t) : Embedding (Set.inclusion h)

theorem DiscreteTopology.of_subset {X : Type u_5} [TopologicalSpace X] {s : Set X} {t : Set X} : DiscreteTopology ↑s → t ⊆ s → DiscreteTopology ↑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.

theorem DiscreteTopology.preimage_of_continuous_injective {X : Type u_5} {Y : Type u_6} [TopologicalSpace X] [TopologicalSpace Y] (s : Set Y) [DiscreteTopology ↑s] {f : X → Y} (hc : Continuous f) (hinj : Function.Injective f) : DiscreteTopology ↑(f ⁻¹' s)

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 : X → Y} (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 : X → X → Prop} : QuotientMap (Quot.mk r)

theorem continuous_quot_mk {X : Type u} [TopologicalSpace X] {r : X → X → Prop} : Continuous (Quot.mk r)

theorem continuous_quot_lift {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {r : X → X → Prop} {f : X → Y} (hr : ∀ (a b : X), r a b → f a = f b) (h : Continuous f) : Continuous (Quot.lift f hr)

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 : X → Y} (h : Continuous f) (hs : ∀ (a b : X), a ≈ b → f a = f b) : Continuous (Quotient.lift f hs)

theorem Continuous.quotient_liftOn' {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Setoid X} {f : X → Y} (h : Continuous f) (hs : ∀ (a b : X), Setoid.r a b → f 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 : X → Y} (hf : Continuous f) (H : (Setoid.r ⇒ Setoid.r) f f) : Continuous (Quotient.map' f H)

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) : Continuous f

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) : ContinuousAt f 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 : ι) → π i → X 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 : X → Y} (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) : Continuous (Set.restrict₂ hst)

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) : Continuous (Finset.restrict₂ hst)

theorem Pi.continuous_restrict_apply {X : Type u} [TopologicalSpace X] {Z : Type u_8} [TopologicalSpace Z] (s : Set X) {f : X → Z} (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 : ↑t → Z} (hf : Continuous f) : Continuous (Set.restrict₂ hst f)

theorem Finset.continuous_restrict_apply {X : Type u} [TopologicalSpace X] {Z : Type u_8} [TopologicalSpace Z] (s : Finset X) {f : X → Z} (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) : Continuous (Finset.restrict₂ hst f)

theorem Pi.induced_restrict {ι : Type u_5} {π : ι → Type u_6} [T : (i : ι) → TopologicalSpace (π i)] (S : Set ι) : TopologicalSpace.induced S.restrict Pi.topologicalSpace = ⨅ i ∈ S, 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 : ∀ a ∈ i, 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 ↔ ∀ f ∈ s, ∃ (I : Finset ι) (u : (a : ι) → Set (π a)), (∀ a ∈ I, 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 ↔ ∀ f ∈ s, ∃ (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 : ∀ a ∈ i, 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 : ∀ a ∈ i, 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 ↔ ∀ i ∈ I, 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 ι), (∀ a ∈ i, 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 ι), (∀ a ∈ i, 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 : ι} : Continuous (Sigma.mk 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 : ι} : IsOpenMap (Sigma.mk i)

theorem isOpen_range_sigmaMk {ι : Type u_5} {σ : ι → Type u_7} [(i : ι) → TopologicalSpace (σ i)] {i : ι} : IsOpen (Set.range (Sigma.mk i))

theorem isClosedMap_sigmaMk {ι : Type u_5} {σ : ι → Type u_7} [(i : ι) → TopologicalSpace (σ i)] {i : ι} : IsClosedMap (Sigma.mk i)

theorem isClosed_range_sigmaMk {ι : Type u_5} {σ : ι → Type u_7} [(i : ι) → TopologicalSpace (σ i)] {i : ι} : IsClosed (Set.range (Sigma.mk i))

theorem openEmbedding_sigmaMk {ι : Type u_5} {σ : ι → Type u_7} [(i : ι) → TopologicalSpace (σ i)] {i : ι} : OpenEmbedding (Sigma.mk i)

theorem closedEmbedding_sigmaMk {ι : Type u_5} {σ : ι → Type u_7} [(i : ι) → TopologicalSpace (σ i)] {i : ι} : ClosedEmbedding (Sigma.mk i)

theorem embedding_sigmaMk {ι : Type u_5} {σ : ι → Type u_7} [(i : ι) → TopologicalSpace (σ i)] {i : ι} : Embedding (Sigma.mk 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⟩) : Continuous f

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 ULift.isClosed_iff {X : Type u} [TopologicalSpace X] {s : Set (ULift.{v, u} X)} : IsClosed s ↔ IsClosed (ULift.up ⁻¹' s)

theorem continuous_uLift_down {X : Type u} [TopologicalSpace X] : Continuous ULift.down

theorem continuous_uLift_up {X : Type u} [TopologicalSpace X] : Continuous ULift.up

theorem embedding_uLift_down {X : Type u} [TopologicalSpace X] : Embedding ULift.down

theorem ULift.closedEmbedding_down {X : Type u} [TopologicalSpace X] : ClosedEmbedding ULift.down

instance instDiscreteTopologyULift {X : Type u} [TopologicalSpace X] [DiscreteTopology X] : DiscreteTopology (ULift.{u_5, u} X)

Equations

• ⋯ = ⋯

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) : nhdsSet (s ×ˢ t) ≤ nhdsSet s ×ˢ nhdsSet t

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 × Y → Prop} : (∀ᶠ (q : X × Y) in nhdsSet (s ×ˢ t), p q) ↔ ∀ x ∈ s, ∀ y ∈ t, ∃ (px : X → Prop), (∀ᶠ (x' : X) in nhds x, px x') ∧ ∃ (py : Y → Prop), (∀ᶠ (y' : Y) in nhds y, py y') ∧ ∀ {x : X}, px x → ∀ {y : Y}, py y → p (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 × Y → Prop} {px : X → Prop} {py : Y → Prop} (hp : ∀ {x : X}, px x → ∀ {y : Y}, py y → p (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