Mathlib.Topology.Constructions.SumProd

instTopologicalSpaceSum instance

[t₁ : TopologicalSpace X] [t₂ : TopologicalSpace Y] : TopologicalSpace (X ⊕ Y)

Full source

instance instTopologicalSpaceSum [t₁ : TopologicalSpace X] [t₂ : TopologicalSpace Y] :
    TopologicalSpace (X ⊕ Y) :=
  coinducedcoinduced Sum.inl t₁ ⊔ coinduced Sum.inr t₂

Topological Space Structure on Disjoint Union

Informal description

For any topological spaces $X$ and $Y$, the disjoint union $X \oplus Y$ is equipped with the canonical topological space structure where a set is open if and only if its preimages under both inclusion maps are open in $X$ and $Y$ respectively.

instTopologicalSpaceProd instance

[t₁ : TopologicalSpace X] [t₂ : TopologicalSpace Y] : TopologicalSpace (X × Y)

Full source

instance instTopologicalSpaceProd [t₁ : TopologicalSpace X] [t₂ : TopologicalSpace Y] :
    TopologicalSpace (X × Y) :=
  inducedinduced Prod.fst t₁ ⊓ induced Prod.snd t₂

Topological Space Structure on Product Spaces

Informal description

For any topological spaces $X$ and $Y$, the product space $X \times Y$ has a canonical topological space structure where the open sets are generated by products of open sets in $X$ and $Y$.

continuous_prodMk theorem

{f : X → Y} {g : X → Z} : (Continuous fun x => (f x, g x)) ↔ Continuous f ∧ Continuous g

Full source

@[simp]
theorem continuous_prodMk {f : X → Y} {g : X → Z} :
    (Continuous fun x => (f x, g x)) ↔ Continuous f ∧ Continuous g :=
  continuous_inf_rng.trans <| continuous_induced_rng.and continuous_induced_rng

Continuity Criterion for Product Maps: $f$ continuous iff $f_1$ and $f_2$ continuous

Informal description

A function $f \colon X \to Y \times Z$ defined by $f(x) = (f_1(x), f_2(x))$ is continuous if and only if both component functions $f_1 \colon X \to Y$ and $f_2 \colon X \to Z$ are continuous.

continuous_fst theorem

: Continuous (@Prod.fst X Y)

Full source

@[continuity]
theorem continuous_fst : Continuous (@Prod.fst X Y) :=
  (continuous_prodMk.1 continuous_id).1

Continuity of the First Projection Map

Informal description

The projection map $\pi_1 \colon X \times Y \to X$ onto the first factor is continuous.

Continuous.fst theorem

{f : X → Y × Z} (hf : Continuous f) : Continuous fun x : X => (f x).1

Full source

/-- Postcomposing `f` with `Prod.fst` is continuous -/
@[fun_prop]
theorem Continuous.fst {f : X → Y × Z} (hf : Continuous f) : Continuous fun x : X => (f x).1 :=
  continuous_fst.comp hf

Continuity of the First Component of a Continuous Product Map

Informal description

Let $X$, $Y$, and $Z$ be topological spaces, and let $f \colon X \to Y \times Z$ be a continuous function. Then the composition of $f$ with the first projection map $\pi_1 \colon Y \times Z \to Y$ is continuous, i.e., the function $x \mapsto (f(x)).1$ is continuous.

Continuous.fst' theorem

{f : X → Z} (hf : Continuous f) : Continuous fun x : X × Y => f x.fst

Full source

/-- Precomposing `f` with `Prod.fst` is continuous -/
theorem Continuous.fst' {f : X → Z} (hf : Continuous f) : Continuous fun x : X × Y => f x.fst :=
  hf.comp continuous_fst

Continuity of First Projection Precomposition

Informal description

Let $X$, $Y$, and $Z$ be topological spaces. If $f \colon X \to Z$ is a continuous function, then the function $g \colon X \times Y \to Z$ defined by $g(x,y) = f(x)$ is also continuous.

continuousAt_fst theorem

{p : X × Y} : ContinuousAt Prod.fst p

Full source

theorem continuousAt_fst {p : X × Y} : ContinuousAt Prod.fst p :=
  continuous_fst.continuousAt

Continuity of First Projection at a Point in Product Space

Informal description

For any point $p = (x, y)$ in the product space $X \times Y$, the projection map $\pi_1 \colon X \times Y \to X$ onto the first factor is continuous at $p$.

ContinuousAt.fst theorem

{f : X → Y × Z} {x : X} (hf : ContinuousAt f x) : ContinuousAt (fun x : X => (f x).1) x

Full source

/-- Postcomposing `f` with `Prod.fst` is continuous at `x` -/
@[fun_prop]
theorem ContinuousAt.fst {f : X → Y × Z} {x : X} (hf : ContinuousAt f x) :
    ContinuousAt (fun x : X => (f x).1) x :=
  continuousAt_fst.comp hf

Continuity of First Projection under Composition at a Point

Informal description

Let $X$, $Y$, and $Z$ be topological spaces, and let $f \colon X \to Y \times Z$ be a function. If $f$ is continuous at a point $x \in X$, then the composition of $f$ with the first projection $\pi_1 \colon Y \times Z \to Y$ is also continuous at $x$. In other words, the function $x \mapsto (f(x))_1$ is continuous at $x$.

ContinuousAt.fst' theorem

{f : X → Z} {x : X} {y : Y} (hf : ContinuousAt f x) : ContinuousAt (fun x : X × Y => f x.fst) (x, y)

Full source

/-- Precomposing `f` with `Prod.fst` is continuous at `(x, y)` -/
theorem ContinuousAt.fst' {f : X → Z} {x : X} {y : Y} (hf : ContinuousAt f x) :
    ContinuousAt (fun x : X × Y => f x.fst) (x, y) :=
  ContinuousAt.comp hf continuousAt_fst

Continuity of First-Projection-Precomposition at a Point in Product Space

Informal description

Let $X$, $Y$, and $Z$ be topological spaces, and let $f \colon X \to Z$ be a function that is continuous at a point $x \in X$. Then the function $F \colon X \times Y \to Z$ defined by $F(x,y) = f(x)$ is continuous at the point $(x,y) \in X \times Y$.

ContinuousAt.fst'' theorem

{f : X → Z} {x : X × Y} (hf : ContinuousAt f x.fst) : ContinuousAt (fun x : X × Y => f x.fst) x

Full source

/-- Precomposing `f` with `Prod.fst` is continuous at `x : X × Y` -/
theorem ContinuousAt.fst'' {f : X → Z} {x : X × Y} (hf : ContinuousAt f x.fst) :
    ContinuousAt (fun x : X × Y => f x.fst) x :=
  hf.comp continuousAt_fst

Continuity of First Projection Precomposition at a Point in Product Space

Informal description

Let $X$, $Y$, and $Z$ be topological spaces, and let $f \colon X \to Z$ be a function. For any point $x = (x_1, x_2) \in X \times Y$, if $f$ is continuous at $x_1$, then the function $(x, y) \mapsto f(x)$ is continuous at $x$.

Filter.Tendsto.fst_nhds theorem

 {X} {l : Filter X} {f : X → Y × Z} {p : Y × Z} (h : Tendsto f l (𝓝 p)) : Tendsto (fun a ↦ (f a).1) l (𝓝 <| p.1)

Full source

theorem Filter.Tendsto.fst_nhds {X} {l : Filter X} {f : X → Y × Z} {p : Y × Z}
    (h : Tendsto f l (𝓝 p)) : Tendsto (fun a ↦ (f a).1) l (𝓝 <| p.1) :=
  continuousAt_fst.tendsto.comp h

Limit of First Component in Product Space

Informal description

Let $X$, $Y$, and $Z$ be topological spaces, and let $f \colon X \to Y \times Z$ be a function. If $f$ tends to a point $p = (p_1, p_2) \in Y \times Z$ as the input tends to some limit $l$ (in the sense of filters), then the first component function $x \mapsto (f(x)).1$ tends to $p_1$ as the input tends to $l$.

continuous_snd theorem

: Continuous (@Prod.snd X Y)

Full source

@[continuity]
theorem continuous_snd : Continuous (@Prod.snd X Y) :=
  (continuous_prodMk.1 continuous_id).2

Continuity of the Second Projection Map

Informal description

The second projection map $\text{snd} \colon X \times Y \to Y$ is continuous.

Continuous.snd theorem

{f : X → Y × Z} (hf : Continuous f) : Continuous fun x : X => (f x).2

Full source

/-- Postcomposing `f` with `Prod.snd` is continuous -/
@[fun_prop]
theorem Continuous.snd {f : X → Y × Z} (hf : Continuous f) : Continuous fun x : X => (f x).2 :=
  continuous_snd.comp hf

Continuity of the Second Component of a Continuous Map into a Product Space

Informal description

Let $X$, $Y$, and $Z$ be topological spaces. If a function $f \colon X \to Y \times Z$ is continuous, then the function $x \mapsto (f(x)).2$ (the composition of $f$ with the second projection) is continuous.

Continuous.snd' theorem

{f : Y → Z} (hf : Continuous f) : Continuous fun x : X × Y => f x.snd

Full source

/-- Precomposing `f` with `Prod.snd` is continuous -/
theorem Continuous.snd' {f : Y → Z} (hf : Continuous f) : Continuous fun x : X × Y => f x.snd :=
  hf.comp continuous_snd

Continuity of Precomposition with Second Projection

Informal description

Let $X$ and $Y$ be topological spaces, and let $f \colon Y \to Z$ be a continuous function. Then the function $g \colon X \times Y \to Z$ defined by $g(x,y) = f(y)$ is continuous.

continuousAt_snd theorem

{p : X × Y} : ContinuousAt Prod.snd p

Full source

theorem continuousAt_snd {p : X × Y} : ContinuousAt Prod.snd p :=
  continuous_snd.continuousAt

Pointwise Continuity of the Second Projection Map

Informal description

For any point $p = (x, y)$ in the product topological space $X \times Y$, the second projection map $\text{snd} \colon X \times Y \to Y$ is continuous at $p$.

ContinuousAt.snd theorem

{f : X → Y × Z} {x : X} (hf : ContinuousAt f x) : ContinuousAt (fun x : X => (f x).2) x

Full source

/-- Postcomposing `f` with `Prod.snd` is continuous at `x` -/
@[fun_prop]
theorem ContinuousAt.snd {f : X → Y × Z} {x : X} (hf : ContinuousAt f x) :
    ContinuousAt (fun x : X => (f x).2) x :=
  continuousAt_snd.comp hf

Continuity of the Second Component at a Point

Informal description

Let $X$, $Y$, and $Z$ be topological spaces, and let $f \colon X \to Y \times Z$ be a function that is continuous at a point $x \in X$. Then the function $g \colon X \to Z$ defined by $g(x) = \text{snd}(f(x))$ (i.e., the second component of $f(x)$) is continuous at $x$.

ContinuousAt.snd' theorem

{f : Y → Z} {x : X} {y : Y} (hf : ContinuousAt f y) : ContinuousAt (fun x : X × Y => f x.snd) (x, y)

Full source

/-- Precomposing `f` with `Prod.snd` is continuous at `(x, y)` -/
theorem ContinuousAt.snd' {f : Y → Z} {x : X} {y : Y} (hf : ContinuousAt f y) :
    ContinuousAt (fun x : X × Y => f x.snd) (x, y) :=
  ContinuousAt.comp hf continuousAt_snd

Continuity of Second Projection Precomposition at a Point

Informal description

Let $X$, $Y$, and $Z$ be topological spaces, and let $f \colon Y \to Z$ be a function that is continuous at a point $y \in Y$. Then the function $(x, y') \mapsto f(y')$ from $X \times Y$ to $Z$ is continuous at the point $(x, y) \in X \times Y$.

ContinuousAt.snd'' theorem

{f : Y → Z} {x : X × Y} (hf : ContinuousAt f x.snd) : ContinuousAt (fun x : X × Y => f x.snd) x

Full source

/-- Precomposing `f` with `Prod.snd` is continuous at `x : X × Y` -/
theorem ContinuousAt.snd'' {f : Y → Z} {x : X × Y} (hf : ContinuousAt f x.snd) :
    ContinuousAt (fun x : X × Y => f x.snd) x :=
  hf.comp continuousAt_snd

Continuity of Second Projection Precomposition at a Point

Informal description

Let $X$, $Y$, and $Z$ be topological spaces, and let $f \colon Y \to Z$ be a function. For any point $x = (x_1, x_2) \in X \times Y$, if $f$ is continuous at $x_2 \in Y$, then the function $g \colon X \times Y \to Z$ defined by $g(x) = f(x_2)$ is continuous at $x$.

Filter.Tendsto.snd_nhds theorem

 {X} {l : Filter X} {f : X → Y × Z} {p : Y × Z} (h : Tendsto f l (𝓝 p)) : Tendsto (fun a ↦ (f a).2) l (𝓝 <| p.2)

Full source

theorem Filter.Tendsto.snd_nhds {X} {l : Filter X} {f : X → Y × Z} {p : Y × Z}
    (h : Tendsto f l (𝓝 p)) : Tendsto (fun a ↦ (f a).2) l (𝓝 <| p.2) :=
  continuousAt_snd.tendsto.comp h

Limit Preservation of Second Projection under Product-Valued Functions

Informal description

Let $X$, $Y$, and $Z$ be topological spaces, and let $f \colon X \to Y \times Z$ be a function. If $f$ tends to a point $p = (p_1, p_2) \in Y \times Z$ as $x$ tends to some limit in $X$ (with respect to the neighborhood filters), then the second component function $x \mapsto (f(x)).2$ tends to $p_2$ as $x$ tends to the same limit.

Continuous.prodMk theorem

{f : Z → X} {g : Z → Y} (hf : Continuous f) (hg : Continuous g) : Continuous fun x => (f x, g x)

Full source

@[continuity, fun_prop]
theorem Continuous.prodMk {f : Z → X} {g : Z → Y} (hf : Continuous f) (hg : Continuous g) :
    Continuous fun x => (f x, g x) :=
  continuous_prodMk.2 ⟨hf, hg⟩

Continuity of Product Maps

Informal description

Let $f \colon Z \to X$ and $g \colon Z \to Y$ be continuous functions between topological spaces. Then the product map $(f, g) \colon Z \to X \times Y$ defined by $(f, g)(z) = (f(z), g(z))$ is continuous.

Continuous.prodMk_right theorem

(x : X) : Continuous fun y : Y => (x, y)

Full source

@[continuity]
theorem Continuous.prodMk_right (x : X) : Continuous fun y : Y => (x, y) := by fun_prop

Continuity of the Right Product Map with Fixed First Coordinate

Informal description

For any topological spaces $X$ and $Y$, and any fixed element $x \in X$, the function $f \colon Y \to X \times Y$ defined by $f(y) = (x, y)$ is continuous.

Continuous.prodMk_left theorem

(y : Y) : Continuous fun x : X => (x, y)

Full source

@[continuity]
theorem Continuous.prodMk_left (y : Y) : Continuous fun x : X => (x, y) := by fun_prop

Continuity of the Left Product Map with Fixed Second Coordinate

Informal description

For any topological spaces $X$ and $Y$, and any fixed element $y \in Y$, the function $f \colon X \to X \times Y$ defined by $f(x) = (x, y)$ is continuous.

IsClosed.setOf_mapsTo theorem

 {α : Type*} {f : X → α → Z} {s : Set α} {t : Set Z} (ht : IsClosed t) (hf : ∀ a ∈ s, Continuous (f · a)) :
  IsClosed {x | MapsTo (f x) s t}

Full source

/-- 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. -/
lemma IsClosed.setOf_mapsTo {α : Type*} {f : X → α → Z} {s : Set α} {t : Set Z} (ht : IsClosed t)
    (hf : ∀ a ∈ s, Continuous (f · a)) : IsClosed {x | MapsTo (f x) s t} := by
  simpa only [MapsTo, setOf_forall] using isClosed_biInter fun y hy ↦ ht.preimage (hf y hy)

Closedness of the Set Where a Family of Continuous Functions Maps into a Closed Set

Informal description

Let $X$ and $Z$ be topological spaces, and let $\alpha$ be an arbitrary type. Given a function $f \colon X \to (\alpha \to Z)$, a subset $s \subseteq \alpha$, and a closed subset $t \subseteq Z$, if for every $a \in s$ the function $f(\cdot)(a) \colon X \to Z$ is continuous, then the set $\{x \in X \mid f(x) \text{ maps } s \text{ into } t\}$ is closed in $X$.

Continuous.comp₂ theorem

 {g : X × Y → Z} (hg : Continuous g) {e : W → X} (he : Continuous e) {f : W → Y} (hf : Continuous f) :
  Continuous fun w => g (e w, f w)

Full source

theorem Continuous.comp₂ {g : X × Y → Z} (hg : Continuous g) {e : W → X} (he : Continuous e)
    {f : W → Y} (hf : Continuous f) : Continuous fun w => g (e w, f w) :=
  hg.comp <| he.prodMk hf

Continuity of Binary Composition of Continuous Functions

Informal description

Let $X$, $Y$, $Z$, and $W$ be topological spaces. Given a continuous function $g \colon X \times Y \to Z$ and continuous functions $e \colon W \to X$ and $f \colon W \to Y$, the function $h \colon W \to Z$ defined by $h(w) = g(e(w), f(w))$ is continuous.

Continuous.comp₃ theorem

 {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 => g (e w, f w, k w)

Full source

theorem Continuous.comp₃ {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 => g (e w, f w, k w) :=
  hg.comp₂ he <| hf.prodMk hk

Continuity of Ternary Composition of Continuous Functions

Informal description

Let $X$, $Y$, $Z$, $\varepsilon$, and $W$ be topological spaces. Given a continuous function $g \colon X \times Y \times Z \to \varepsilon$ and continuous functions $e \colon W \to X$, $f \colon W \to Y$, and $k \colon W \to Z$, the function $h \colon W \to \varepsilon$ defined by $h(w) = g(e(w), f(w), k(w))$ is continuous.

Continuous.comp₄ theorem

 {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 => g (e w, f w, k w, l w)

Full source

theorem Continuous.comp₄ {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 => g (e w, f w, k w, l w) :=
  hg.comp₃ he hf <| hk.prodMk hl

Continuity of Quaternary Composition of Continuous Functions

Informal description

Let $X$, $Y$, $Z$, $\zeta$, $\varepsilon$, and $W$ be topological spaces. Given a continuous function $g \colon X \times Y \times Z \times \zeta \to \varepsilon$ and continuous functions $e \colon W \to X$, $f \colon W \to Y$, $k \colon W \to Z$, and $l \colon W \to \zeta$, the function $h \colon W \to \varepsilon$ defined by $h(w) = g(e(w), f(w), k(w), l(w))$ is continuous.

Continuous.prodMap theorem

{f : Z → X} {g : W → Y} (hf : Continuous f) (hg : Continuous g) : Continuous (Prod.map f g)

Full source

@[continuity, fun_prop]
theorem Continuous.prodMap {f : Z → X} {g : W → Y} (hf : Continuous f) (hg : Continuous g) :
    Continuous (Prod.map f g) :=
  hf.fst'.prodMk hg.snd'

Continuity of Product Maps: $f \times g$ is Continuous When $f$ and $g$ Are Continuous

Informal description

Let $f \colon Z \to X$ and $g \colon W \to Y$ be continuous functions between topological spaces. Then the product map $f \times g \colon Z \times W \to X \times Y$ defined by $(f \times g)(z,w) = (f(z), g(w))$ is continuous.

continuous_inf_dom_left₂ theorem

 {X Y Z} {f : X → Y → Z} {ta1 ta2 : TopologicalSpace X} {tb1 tb2 : TopologicalSpace Y} {tc1 : TopologicalSpace Z}
  (h : by haveI := ta1; haveI := tb1; exact Continuous fun p : X × Y => f p.1 p.2) : by haveI := ta1 ⊓ ta2;
  haveI := tb1 ⊓ tb2; exact Continuous fun p : X × Y => f p.1 p.2

Full source

/-- A version of `continuous_inf_dom_left` for binary functions -/
theorem continuous_inf_dom_left₂ {X Y Z} {f : X → Y → Z} {ta1 ta2 : TopologicalSpace X}
    {tb1 tb2 : TopologicalSpace Y} {tc1 : TopologicalSpace Z}
    (h : by haveI := ta1; haveI := tb1; exact Continuous fun p : X × Y => f p.1 p.2) : by
    haveI := ta1 ⊓ ta2; haveI := tb1 ⊓ tb2; exact Continuous fun p : X × Y => f p.1 p.2 := by
  have ha := @continuous_inf_dom_left _ _ id ta1 ta2 ta1 (@continuous_id _ (id _))
  have hb := @continuous_inf_dom_left _ _ id tb1 tb2 tb1 (@continuous_id _ (id _))
  have h_continuous_id := @Continuous.prodMap _ _ _ _ ta1 tb1 (ta1 ⊓ ta2) (tb1 ⊓ tb2) _ _ ha hb
  exact @Continuous.comp _ _ _ (id _) (id _) _ _ _ h h_continuous_id

Continuity of Binary Functions Under Infimum Domain Topologies (Left Variant)

Informal description

Let $X$, $Y$, and $Z$ be topological spaces with two topologies $t_{a1}, t_{a2}$ on $X$ and $t_{b1}, t_{b2}$ on $Y$. Let $f \colon X \times Y \to Z$ be a function. If $f$ is continuous when $X$ is equipped with $t_{a1}$ and $Y$ is equipped with $t_{b1}$, then $f$ is also continuous when $X$ is equipped with the infimum topology $t_{a1} \sqcap t_{a2}$ and $Y$ is equipped with the infimum topology $t_{b1} \sqcap t_{b2}$.

continuous_inf_dom_right₂ theorem

 {X Y Z} {f : X → Y → Z} {ta1 ta2 : TopologicalSpace X} {tb1 tb2 : TopologicalSpace Y} {tc1 : TopologicalSpace Z}
  (h : by haveI := ta2; haveI := tb2; exact Continuous fun p : X × Y => f p.1 p.2) : by haveI := ta1 ⊓ ta2;
  haveI := tb1 ⊓ tb2; exact Continuous fun p : X × Y => f p.1 p.2

Full source

/-- A version of `continuous_inf_dom_right` for binary functions -/
theorem continuous_inf_dom_right₂ {X Y Z} {f : X → Y → Z} {ta1 ta2 : TopologicalSpace X}
    {tb1 tb2 : TopologicalSpace Y} {tc1 : TopologicalSpace Z}
    (h : by haveI := ta2; haveI := tb2; exact Continuous fun p : X × Y => f p.1 p.2) : by
    haveI := ta1 ⊓ ta2; haveI := tb1 ⊓ tb2; exact Continuous fun p : X × Y => f p.1 p.2 := by
  have ha := @continuous_inf_dom_right _ _ id ta1 ta2 ta2 (@continuous_id _ (id _))
  have hb := @continuous_inf_dom_right _ _ id tb1 tb2 tb2 (@continuous_id _ (id _))
  have h_continuous_id := @Continuous.prodMap _ _ _ _ ta2 tb2 (ta1 ⊓ ta2) (tb1 ⊓ tb2) _ _ ha hb
  exact @Continuous.comp _ _ _ (id _) (id _) _ _ _ h h_continuous_id

Continuity Preservation Under Infimum Topologies (Right Variant)

Informal description

Let $X$, $Y$, and $Z$ be topological spaces, and let $f \colon X \times Y \to Z$ be a function. Suppose $f$ is continuous when $X$ is equipped with topology $ta2$ and $Y$ is equipped with topology $tb2$. Then $f$ remains continuous when $X$ is equipped with the infimum topology $ta1 \sqcap ta2$ and $Y$ is equipped with the infimum topology $tb1 \sqcap tb2$.

continuous_sInf_dom₂ theorem

 {X Y Z} {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) : by
  haveI := sInf tas; haveI := sInf tbs
  exact @Continuous _ _ _ tc fun p : X × Y => f p.1 p.2

Full source

/-- A version of `continuous_sInf_dom` for binary functions -/
theorem continuous_sInf_dom₂ {X Y Z} {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) : by
    haveI := sInf tas; haveI := sInf tbs
    exact @Continuous _ _ _ tc fun p : X × Y => f p.1 p.2 := by
  have hX := continuous_sInf_dom hX continuous_id
  have hY := continuous_sInf_dom hY continuous_id
  have h_continuous_id := @Continuous.prodMap _ _ _ _ tX tY (sInf tas) (sInf tbs) _ _ hX hY
  exact @Continuous.comp _ _ _ (id _) (id _) _ _ _ hf h_continuous_id

Continuity of Binary Functions Under Infimum of Domain Topologies

Informal description

Let $X$, $Y$, and $Z$ be topological spaces, and let $f \colon X \times Y \to Z$ be a function. Given collections of topologies $\mathcal{T}_X$ on $X$ and $\mathcal{T}_Y$ on $Y$, suppose there exist topologies $t_X \in \mathcal{T}_X$ and $t_Y \in \mathcal{T}_Y$ such that $f$ is continuous with respect to $t_X \times t_Y$ and $t_Z$. Then $f$ is also continuous with respect to the infimum topologies $\bigsqcap \mathcal{T}_X$ on $X$, $\bigsqcap \mathcal{T}_Y$ on $Y$, and $t_Z$ on $Z$.

Filter.Eventually.prod_inl_nhds theorem

{p : X → Prop} {x : X} (h : ∀ᶠ x in 𝓝 x, p x) (y : Y) : ∀ᶠ x in 𝓝 (x, y), p (x : X × Y).1

Full source

theorem Filter.Eventually.prod_inl_nhds {p : X → Prop} {x : X} (h : ∀ᶠ x in 𝓝 x, p x) (y : Y) :
    ∀ᶠ x in 𝓝 (x, y), p (x : X × Y).1 :=
  continuousAt_fst h

Persistence of Eventual Property Under First Projection in Product Space

Informal description

Let $X$ and $Y$ be topological spaces. For any predicate $p$ on $X$ and any point $x \in X$, if $p$ holds eventually in the neighborhood filter of $x$, then for any $y \in Y$, the predicate $p$ holds eventually in the neighborhood filter of $(x,y)$ when applied to the first component.

Filter.Eventually.prod_inr_nhds theorem

{p : Y → Prop} {y : Y} (h : ∀ᶠ x in 𝓝 y, p x) (x : X) : ∀ᶠ x in 𝓝 (x, y), p (x : X × Y).2

Full source

theorem Filter.Eventually.prod_inr_nhds {p : Y → Prop} {y : Y} (h : ∀ᶠ x in 𝓝 y, p x) (x : X) :
    ∀ᶠ x in 𝓝 (x, y), p (x : X × Y).2 :=
  continuousAt_snd h

Eventual Preservation of Property in Second Component of Product Neighborhood

Informal description

For any property $p$ on $Y$ and any point $y \in Y$, if $p$ holds eventually in the neighborhood filter of $y$, then for any point $x \in X$, the property $p$ holds eventually in the neighborhood filter of $(x, y)$ when applied to the second component of the pair.

Filter.Eventually.prodMk_nhds theorem

 {px : X → Prop} {x} (hx : ∀ᶠ x in 𝓝 x, px x) {py : Y → Prop} {y} (hy : ∀ᶠ y in 𝓝 y, py y) :
  ∀ᶠ p in 𝓝 (x, y), px (p : X × Y).1 ∧ py p.2

Full source

theorem Filter.Eventually.prodMk_nhds {px : X → Prop} {x} (hx : ∀ᶠ x in 𝓝 x, px x) {py : Y → Prop}
    {y} (hy : ∀ᶠ y in 𝓝 y, py y) : ∀ᶠ p in 𝓝 (x, y), px (p : X × Y).1 ∧ py p.2 :=
  (hx.prod_inl_nhds y).and (hy.prod_inr_nhds x)

Eventual Preservation of Properties in Product Neighborhood Filter

Informal description

Let $X$ and $Y$ be topological spaces. For any predicates $p_X$ on $X$ and $p_Y$ on $Y$, if $p_X$ holds eventually in the neighborhood filter of $x \in X$ and $p_Y$ holds eventually in the neighborhood filter of $y \in Y$, then the conjunction $p_X(x') \land p_Y(y')$ holds eventually in the neighborhood filter of $(x, y) \in X \times Y$ for all $(x', y')$ in the neighborhood.

continuous_swap theorem

: Continuous (Prod.swap : X × Y → Y × X)

Full source

theorem continuous_swap : Continuous (Prod.swap : X × Y → Y × X) :=
  continuous_snd.prodMk continuous_fst

Continuity of the Swap Map on Product Spaces

Informal description

The swap function $(x, y) \mapsto (y, x)$ from the product topological space $X \times Y$ to $Y \times X$ is continuous.

isClosedMap_swap theorem

: IsClosedMap (Prod.swap : X × Y → Y × X)

Full source

lemma isClosedMap_swap : IsClosedMap (Prod.swap : X × Y → Y × X) := fun s hs ↦ by
  rw [image_swap_eq_preimage_swap]
  exact hs.preimage continuous_swap

Swap Map is Closed on Product Spaces

Informal description

The swap function $(x, y) \mapsto (y, x)$ from the product topological space $X \times Y$ to $Y \times X$ is a closed map, meaning that for every closed subset $C \subseteq X \times Y$, the image $\text{swap}(C)$ is closed in $Y \times X$.

Continuous.uncurry_left theorem

{f : X → Y → Z} (x : X) (h : Continuous (uncurry f)) : Continuous (f x)

Full source

theorem Continuous.uncurry_left {f : X → Y → Z} (x : X) (h : Continuous (uncurry f)) :
    Continuous (f x) :=
  h.comp (.prodMk_right _)

Continuity of Partially Applied Function from Uncurried Continuous Function

Informal description

Let $X$, $Y$, and $Z$ be topological spaces, and let $f \colon X \to Y \to Z$ be a function such that the uncurried function $F \colon X \times Y \to Z$ defined by $F(x, y) = f(x)(y)$ is continuous. Then for any fixed $x \in X$, the function $f(x) \colon Y \to Z$ is continuous.

Continuous.uncurry_right theorem

{f : X → Y → Z} (y : Y) (h : Continuous (uncurry f)) : Continuous fun a => f a y

Full source

theorem Continuous.uncurry_right {f : X → Y → Z} (y : Y) (h : Continuous (uncurry f)) :
    Continuous fun a => f a y :=
  h.comp (.prodMk_left _)

Continuity of Partially Applied Function from Continuous Uncurried Function

Informal description

Let $X$, $Y$, and $Z$ be topological spaces, and let $f \colon X \to Y \to Z$ be a function such that the uncurried function $(x, y) \mapsto f(x)(y)$ is continuous. Then for any fixed $y \in Y$, the function $x \mapsto f(x)(y)$ is continuous.

continuous_curry theorem

{g : X × Y → Z} (x : X) (h : Continuous g) : Continuous (curry g x)

Full source

theorem continuous_curry {g : X × Y → Z} (x : X) (h : Continuous g) : Continuous (curry g x) :=
  Continuous.uncurry_left x h

Continuity of Curried Function from Continuous Function on Product Space

Informal description

Let $X$, $Y$, and $Z$ be topological spaces, and let $g \colon X \times Y \to Z$ be a continuous function. Then for any fixed $x \in X$, the curried function $g(x, \cdot) \colon Y \to Z$ is continuous.

IsOpen.prod theorem

{s : Set X} {t : Set Y} (hs : IsOpen s) (ht : IsOpen t) : IsOpen (s ×ˢ t)

Full source

theorem IsOpen.prod {s : Set X} {t : Set Y} (hs : IsOpen s) (ht : IsOpen t) : IsOpen (s ×ˢ t) :=
  (hs.preimage continuous_fst).inter (ht.preimage continuous_snd)

Product of Open Sets is Open in Product Topology

Informal description

For any topological spaces $X$ and $Y$, if $s \subseteq X$ and $t \subseteq Y$ are open sets, then their Cartesian product $s \times t$ is open in the product space $X \times Y$.

nhds_prod_eq theorem

{x : X} {y : Y} : 𝓝 (x, y) = 𝓝 x ×ˢ 𝓝 y

Full source

theorem nhds_prod_eq {x : X} {y : Y} : 𝓝 (x, y) = 𝓝 x ×ˢ 𝓝 y := by
  rw [prod_eq_inf, instTopologicalSpaceProd, nhds_inf (t₁ := TopologicalSpace.induced Prod.fst _)
    (t₂ := TopologicalSpace.induced Prod.snd _), nhds_induced, nhds_induced]

Neighborhood Filter of Product Space Equals Product of Neighborhood Filters

Informal description

For any topological spaces $X$ and $Y$, and any points $x \in X$ and $y \in Y$, the neighborhood filter of the point $(x, y)$ in the product space $X \times Y$ is equal to the product of the neighborhood filters of $x$ in $X$ and $y$ in $Y$. In symbols: \[ \mathcal{N}(x, y) = \mathcal{N}(x) \times \mathcal{N}(y) \] where $\mathcal{N}(x, y)$ denotes the neighborhood filter at $(x, y)$ in $X \times Y$, and $\mathcal{N}(x)$, $\mathcal{N}(y)$ denote the neighborhood filters at $x$ and $y$ in $X$ and $Y$ respectively.

nhdsWithin_prod_eq theorem

(x : X) (y : Y) (s : Set X) (t : Set Y) : 𝓝[s ×ˢ t] (x, y) = 𝓝[s] x ×ˢ 𝓝[t] y

Full source

theorem nhdsWithin_prod_eq (x : X) (y : Y) (s : Set X) (t : Set Y) :
    𝓝[s ×ˢ t] (x, y) = 𝓝[s] x ×ˢ 𝓝[t] y := by
  simp only [nhdsWithin, nhds_prod_eq, ← prod_inf_prod, prod_principal_principal]

Neighborhood Filter within Product Set Equals Product of Neighborhood Filters

Informal description

For any topological spaces $X$ and $Y$, points $x \in X$ and $y \in Y$, and subsets $s \subseteq X$ and $t \subseteq Y$, the neighborhood filter within the product set $s \times t$ at the point $(x, y)$ in the product space $X \times Y$ is equal to the product of the neighborhood filters within $s$ at $x$ in $X$ and within $t$ at $y$ in $Y$. In symbols: \[ \mathcal{N}_{s \times t}(x, y) = \mathcal{N}_s(x) \times \mathcal{N}_t(y) \] where $\mathcal{N}_{s \times t}(x, y)$ denotes the neighborhood filter within $s \times t$ at $(x, y)$, and $\mathcal{N}_s(x)$, $\mathcal{N}_t(y)$ denote the neighborhood filters within $s$ at $x$ and within $t$ at $y$ respectively.

Prod.instNeBotNhdsWithinIio instance

[Preorder X] [Preorder Y] {x : X × Y} [hx₁ : (𝓝[<] x.1).NeBot] [hx₂ : (𝓝[<] x.2).NeBot] : (𝓝[<] x).NeBot

Full source

instance Prod.instNeBotNhdsWithinIio [Preorder X] [Preorder Y] {x : X × Y}
    [hx₁ : (𝓝[<] x.1).NeBot] [hx₂ : (𝓝[<] x.2).NeBot] : (𝓝[<] x).NeBot := by
  refine (hx₁.prod hx₂).mono ?_
  rw [← nhdsWithin_prod_eq]
  exact nhdsWithin_mono _ fun _ ⟨h₁, h₂⟩ ↦ Prod.lt_iff.2 <| .inl ⟨h₁, h₂.le⟩

Non-triviality of Neighborhood Filters in Product of Left-infinite Intervals

Informal description

For any preordered spaces $X$ and $Y$, and any point $x = (x_1, x_2)$ in the product space $X \times Y$, if the neighborhood filters within the left-infinite right-open intervals $(-\infty, x_1)$ in $X$ and $(-\infty, x_2)$ in $Y$ are both non-trivial (i.e., contain non-empty sets), then the neighborhood filter within the left-infinite right-open interval $(-\infty, x)$ in $X \times Y$ is also non-trivial.

Prod.instNeBotNhdsWithinIoi instance

[Preorder X] [Preorder Y] {x : X × Y} [hx₁ : (𝓝[>] x.1).NeBot] [hx₂ : (𝓝[>] x.2).NeBot] : (𝓝[>] x).NeBot

Full source

instance Prod.instNeBotNhdsWithinIoi [Preorder X] [Preorder Y] {x : X × Y}
    [hx₁ : (𝓝[>] x.1).NeBot] [hx₂ : (𝓝[>] x.2).NeBot] : (𝓝[>] x).NeBot := by
  refine (hx₁.prod hx₂).mono ?_
  rw [← nhdsWithin_prod_eq]
  exact nhdsWithin_mono _ fun _ ⟨h₁, h₂⟩ ↦ Prod.lt_iff.2 <| .inl ⟨h₁, h₂.le⟩

Nonemptiness of Neighborhood Filters in Product Spaces for Strictly Greater Points

Informal description

For any preordered spaces $X$ and $Y$ and any point $x = (x_1, x_2) \in X \times Y$, if the neighborhood filters $\mathcal{N}_{>x_1}$ and $\mathcal{N}_{>x_2}$ are nonempty (i.e., contain nontrivial sets), then the neighborhood filter $\mathcal{N}_{>x}$ in the product space $X \times Y$ is also nonempty.

mem_nhds_prod_iff theorem

{x : X} {y : Y} {s : Set (X × Y)} : s ∈ 𝓝 (x, y) ↔ ∃ u ∈ 𝓝 x, ∃ v ∈ 𝓝 y, u ×ˢ v ⊆ s

Full source

theorem mem_nhds_prod_iff {x : X} {y : Y} {s : Set (X × Y)} :
    s ∈ 𝓝 (x, y)s ∈ 𝓝 (x, y) ↔ ∃ u ∈ 𝓝 x, ∃ v ∈ 𝓝 y, u ×ˢ v ⊆ s := by rw [nhds_prod_eq, mem_prod_iff]

Characterization of Neighborhoods in Product Topology

Informal description

For any topological spaces $X$ and $Y$, points $x \in X$ and $y \in Y$, and a set $s \subseteq X \times Y$, the set $s$ is a neighborhood of $(x, y)$ in the product topology if and only if there exist neighborhoods $u$ of $x$ in $X$ and $v$ of $y$ in $Y$ such that the product set $u \times v$ is contained in $s$. In symbols: \[ s \in \mathcal{N}(x, y) \iff \exists u \in \mathcal{N}(x), \exists v \in \mathcal{N}(y), u \times v \subseteq s \] where $\mathcal{N}(x, y)$ denotes the neighborhood filter at $(x, y)$ in $X \times Y$, and $\mathcal{N}(x)$, $\mathcal{N}(y)$ denote the neighborhood filters at $x$ and $y$ in $X$ and $Y$ respectively.

mem_nhdsWithin_prod_iff theorem

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

Full source

theorem mem_nhdsWithin_prod_iff {x : X} {y : Y} {s : Set (X × Y)} {tx : Set X} {ty : Set Y} :
    s ∈ 𝓝[tx ×ˢ ty] (x, y)s ∈ 𝓝[tx ×ˢ ty] (x, y) ↔ ∃ u ∈ 𝓝[tx] x, ∃ v ∈ 𝓝[ty] y, u ×ˢ v ⊆ s := by
  rw [nhdsWithin_prod_eq, mem_prod_iff]

Characterization of Neighborhoods within Product Sets in Product Topology

Informal description

For any topological spaces $X$ and $Y$, points $x \in X$ and $y \in Y$, subsets $tx \subseteq X$ and $ty \subseteq Y$, and a set $s \subseteq X \times Y$, the set $s$ belongs to the neighborhood filter within the product set $tx \times ty$ at the point $(x, y)$ if and only if there exist neighborhoods $u$ of $x$ within $tx$ and $v$ of $y$ within $ty$ such that the product set $u \times v$ is contained in $s$. In symbols: \[ s \in \mathcal{N}_{tx \times ty}(x, y) \iff \exists u \in \mathcal{N}_{tx}(x), \exists v \in \mathcal{N}_{ty}(y), u \times v \subseteq s \] where $\mathcal{N}_{tx \times ty}(x, y)$ denotes the neighborhood filter within $tx \times ty$ at $(x, y)$, and $\mathcal{N}_{tx}(x)$, $\mathcal{N}_{ty}(y)$ denote the neighborhood filters within $tx$ at $x$ and within $ty$ at $y$ respectively.

Filter.HasBasis.prod_nhds theorem

 {ιX ιY : Type*} {px : ιX → Prop} {py : ιY → Prop} {sx : ιX → Set X} {sy : ιY → Set Y} {x : X} {y : Y}
  (hx : (𝓝 x).HasBasis px sx) (hy : (𝓝 y).HasBasis py sy) :
  (𝓝 (x, y)).HasBasis (fun i : ιX × ιY => px i.1 ∧ py i.2) fun i => sx i.1 ×ˢ sy i.2

Full source

theorem Filter.HasBasis.prod_nhds {ιX ιY : Type*} {px : ιX → Prop} {py : ιY → Prop}
    {sx : ιX → Set X} {sy : ιY → Set Y} {x : X} {y : Y} (hx : (𝓝 x).HasBasis px sx)
    (hy : (𝓝 y).HasBasis py sy) :
    (𝓝 (x, y)).HasBasis (fun i : ιX × ιY => px i.1 ∧ py i.2) fun i => sx i.1 ×ˢ sy i.2 := by
  rw [nhds_prod_eq]
  exact hx.prod hy

Product Neighborhood Filter Basis Theorem

Informal description

Let $X$ and $Y$ be topological spaces, and let $x \in X$ and $y \in Y$ be points. Suppose the neighborhood filter $\mathcal{N}(x)$ has a basis $\{s_x(i) \mid i \in \iota_X, p_x(i)\}$ and the neighborhood filter $\mathcal{N}(y)$ has a basis $\{s_y(j) \mid j \in \iota_Y, p_y(j)\}$. Then the neighborhood filter $\mathcal{N}((x, y))$ in the product space $X \times Y$ has a basis consisting of products $s_x(i) \times s_y(j)$ for pairs $(i,j) \in \iota_X \times \iota_Y$ satisfying $p_x(i) \land p_y(j)$.

Filter.HasBasis.prod_nhds' theorem

 {ιX ιY : Type*} {pX : ιX → Prop} {pY : ιY → Prop} {sx : ιX → Set X} {sy : ιY → Set Y} {p : X × Y}
  (hx : (𝓝 p.1).HasBasis pX sx) (hy : (𝓝 p.2).HasBasis pY sy) :
  (𝓝 p).HasBasis (fun i : ιX × ιY => pX i.1 ∧ pY i.2) fun i => sx i.1 ×ˢ sy i.2

Full source

theorem Filter.HasBasis.prod_nhds' {ιX ιY : Type*} {pX : ιX → Prop} {pY : ιY → Prop}
    {sx : ιX → Set X} {sy : ιY → Set Y} {p : X × Y} (hx : (𝓝 p.1).HasBasis pX sx)
    (hy : (𝓝 p.2).HasBasis pY sy) :
    (𝓝 p).HasBasis (fun i : ιX × ιY => pX i.1 ∧ pY i.2) fun i => sx i.1 ×ˢ sy i.2 :=
  hx.prod_nhds hy

Basis for Neighborhood Filter in Product Space via Component Bases

Informal description

Let $X$ and $Y$ be topological spaces, and let $p = (x, y) \in X \times Y$. Suppose the neighborhood filter $\mathcal{N}(x)$ has a basis $\{s_X(i) \mid i \in \iota_X, p_X(i)\}$ and the neighborhood filter $\mathcal{N}(y)$ has a basis $\{s_Y(j) \mid j \in \iota_Y, p_Y(j)\}$. Then the neighborhood filter $\mathcal{N}(p)$ in the product space $X \times Y$ has a basis consisting of products $s_X(i) \times s_Y(j)$ for pairs $(i,j) \in \iota_X \times \iota_Y$ satisfying $p_X(i) \land p_Y(j)$.

mem_nhds_prod_iff' theorem

 {x : X} {y : Y} {s : Set (X × Y)} : s ∈ 𝓝 (x, y) ↔ ∃ u v, IsOpen u ∧ x ∈ u ∧ IsOpen v ∧ y ∈ v ∧ u ×ˢ v ⊆ s

Full source

theorem mem_nhds_prod_iff' {x : X} {y : Y} {s : Set (X × Y)} :
    s ∈ 𝓝 (x, y)s ∈ 𝓝 (x, y) ↔ ∃ u v, IsOpen u ∧ x ∈ u ∧ IsOpen v ∧ y ∈ v ∧ u ×ˢ v ⊆ s :=
  ((nhds_basis_opens x).prod_nhds (nhds_basis_opens y)).mem_iff.trans <| by
    simp only [Prod.exists, and_comm, and_assoc, and_left_comm]

Neighborhood Criterion in Product Spaces via Open Rectangles

Informal description

For any point $(x, y)$ in the product space $X \times Y$ and any subset $s \subseteq X \times Y$, $s$ is a neighborhood of $(x, y)$ if and only if there exist open sets $u \subseteq X$ and $v \subseteq Y$ such that $x \in u$, $y \in v$, and the product set $u \times v$ is contained in $s$.

Prod.tendsto_iff theorem

 {X} (seq : X → Y × Z) {f : Filter X} (p : Y × Z) :
  Tendsto seq f (𝓝 p) ↔ Tendsto (fun n => (seq n).fst) f (𝓝 p.fst) ∧ Tendsto (fun n => (seq n).snd) f (𝓝 p.snd)

Full source

theorem Prod.tendsto_iff {X} (seq : X → Y × Z) {f : Filter X} (p : Y × Z) :
    TendstoTendsto seq f (𝓝 p) ↔
      Tendsto (fun n => (seq n).fst) f (𝓝 p.fst) ∧ Tendsto (fun n => (seq n).snd) f (𝓝 p.snd) := by
  rw [nhds_prod_eq, Filter.tendsto_prod_iff']

Characterization of Convergence in Product Spaces via Componentwise Convergence

Informal description

Let $X$, $Y$, and $Z$ be topological spaces, and let $f : X \to Y \times Z$ be a function. For any filter $\mathcal{F}$ on $X$ and any point $p = (y, z) \in Y \times Z$, the function $f$ tends to $p$ along $\mathcal{F}$ if and only if both component functions $\pi_Y \circ f$ and $\pi_Z \circ f$ tend to $y$ and $z$ respectively along $\mathcal{F}$. In symbols: \[ \lim_{\mathcal{F}} f = p \quad \Leftrightarrow \quad \lim_{\mathcal{F}} (\pi_Y \circ f) = y \text{ and } \lim_{\mathcal{F}} (\pi_Z \circ f) = z \] where $\pi_Y$ and $\pi_Z$ are the projection maps from $Y \times Z$ to $Y$ and $Z$ respectively.

instDiscreteTopologyProd instance

[DiscreteTopology X] [DiscreteTopology Y] : DiscreteTopology (X × Y)

Full source

instance [DiscreteTopology X] [DiscreteTopology Y] : DiscreteTopology (X × Y) :=
  discreteTopology_iff_nhds.2 fun (a, b) => by
    rw [nhds_prod_eq, nhds_discrete X, nhds_discrete Y, prod_pure_pure]

Product of Discrete Topological Spaces is Discrete

Informal description

For any topological spaces $X$ and $Y$ with discrete topologies, the product space $X \times Y$ also has the discrete topology.

prod_mem_nhds_iff theorem

{s : Set X} {t : Set Y} {x : X} {y : Y} : s ×ˢ t ∈ 𝓝 (x, y) ↔ s ∈ 𝓝 x ∧ t ∈ 𝓝 y

Full source

theorem prod_mem_nhds_iff {s : Set X} {t : Set Y} {x : X} {y : Y} :
    s ×ˢ t ∈ 𝓝 (x, y)s ×ˢ t ∈ 𝓝 (x, y) ↔ s ∈ 𝓝 x ∧ t ∈ 𝓝 y := by rw [nhds_prod_eq, prod_mem_prod_iff]

Neighborhood Criterion for Product Spaces: $s \times t \in \mathcal{N}(x, y) \leftrightarrow s \in \mathcal{N}(x) \land t \in \mathcal{N}(y)$

Informal description

For any topological spaces $X$ and $Y$, subsets $s \subseteq X$ and $t \subseteq Y$, and points $x \in X$ and $y \in Y$, the Cartesian product $s \times t$ is a neighborhood of $(x, y)$ in the product space $X \times Y$ if and only if $s$ is a neighborhood of $x$ in $X$ and $t$ is a neighborhood of $y$ in $Y$. In symbols: \[ s \times t \in \mathcal{N}(x, y) \leftrightarrow s \in \mathcal{N}(x) \land t \in \mathcal{N}(y) \] where $\mathcal{N}(x, y)$ denotes the neighborhood filter at $(x, y)$ in $X \times Y$, and $\mathcal{N}(x)$, $\mathcal{N}(y)$ denote the neighborhood filters at $x$ and $y$ in $X$ and $Y$ respectively.

prod_mem_nhds theorem

{s : Set X} {t : Set Y} {x : X} {y : Y} (hx : s ∈ 𝓝 x) (hy : t ∈ 𝓝 y) : s ×ˢ t ∈ 𝓝 (x, y)

Full source

theorem prod_mem_nhds {s : Set X} {t : Set Y} {x : X} {y : Y} (hx : s ∈ 𝓝 x) (hy : t ∈ 𝓝 y) :
    s ×ˢ t ∈ 𝓝 (x, y) :=
  prod_mem_nhds_iff.2 ⟨hx, hy⟩

Product of Neighborhoods is Neighborhood in Product Space

Informal description

For any topological spaces $X$ and $Y$, subsets $s \subseteq X$ and $t \subseteq Y$, and points $x \in X$ and $y \in Y$, if $s$ is a neighborhood of $x$ and $t$ is a neighborhood of $y$, then the Cartesian product $s \times t$ is a neighborhood of $(x, y)$ in the product space $X \times Y$. In symbols: \[ s \in \mathcal{N}(x) \land t \in \mathcal{N}(y) \implies s \times t \in \mathcal{N}(x, y) \] where $\mathcal{N}(x, y)$ denotes the neighborhood filter at $(x, y)$ in $X \times Y$, and $\mathcal{N}(x)$, $\mathcal{N}(y)$ denote the neighborhood filters at $x$ and $y$ in $X$ and $Y$ respectively.

isOpen_setOf_disjoint_nhds_nhds theorem

: IsOpen {p : X × X | Disjoint (𝓝 p.1) (𝓝 p.2)}

Full source

theorem isOpen_setOf_disjoint_nhds_nhds : IsOpen { p : X × X | Disjoint (𝓝 p.1) (𝓝 p.2) } := by
  simp only [isOpen_iff_mem_nhds, Prod.forall, mem_setOf_eq]
  intro x y h
  obtain ⟨U, hU, V, hV, hd⟩ := ((nhds_basis_opens x).disjoint_iff (nhds_basis_opens y)).mp h
  exact mem_nhds_prod_iff'.mpr ⟨U, V, hU.2, hU.1, hV.2, hV.1, fun ⟨x', y'⟩ ⟨hx', hy'⟩ =>
    disjoint_of_disjoint_of_mem hd (hU.2.mem_nhds hx') (hV.2.mem_nhds hy')⟩

Openness of the Set of Pairs with Disjoint Neighborhoods in a Product Space

Informal description

For any topological space $X$, the set of pairs $(x, y) \in X \times X$ such that the neighborhood filters $\mathcal{N}(x)$ and $\mathcal{N}(y)$ are disjoint is an open subset of the product space $X \times X$.

Filter.Eventually.prod_nhds theorem

 {p : X → Prop} {q : Y → Prop} {x : X} {y : Y} (hx : ∀ᶠ x in 𝓝 x, p x) (hy : ∀ᶠ y in 𝓝 y, q y) :
  ∀ᶠ z : X × Y in 𝓝 (x, y), p z.1 ∧ q z.2

Full source

theorem Filter.Eventually.prod_nhds {p : X → Prop} {q : Y → Prop} {x : X} {y : Y}
    (hx : ∀ᶠ x in 𝓝 x, p x) (hy : ∀ᶠ y in 𝓝 y, q y) : ∀ᶠ z : X × Y in 𝓝 (x, y), p z.1 ∧ q z.2 :=
  prod_mem_nhds hx hy

Eventual Truth Preservation Under Product Mapping in Neighborhood Filters

Informal description

Let $X$ and $Y$ be topological spaces, and let $p : X \to \text{Prop}$ and $q : Y \to \text{Prop}$ be predicates on $X$ and $Y$ respectively. For any points $x \in X$ and $y \in Y$, if $p$ holds eventually in the neighborhood filter of $x$ and $q$ holds eventually in the neighborhood filter of $y$, then the predicate $\lambda z : X \times Y, p(z.1) \land q(z.2)$ holds eventually in the neighborhood filter of $(x, y)$ in the product space $X \times Y$. In symbols: \[ p \text{ holds } \forall^N x \text{ and } q \text{ holds } \forall^N y \implies (\lambda z, p(z.1) \land q(z.2)) \text{ holds } \forall^N (x, y) \] where $\forall^N a$ denotes "for all points in some neighborhood of $a$".

Filter.EventuallyEq.prodMap_nhds theorem

 {α β : Type*} {f₁ f₂ : X → α} {g₁ g₂ : Y → β} {x : X} {y : Y} (hf : f₁ =ᶠ[𝓝 x] f₂) (hg : g₁ =ᶠ[𝓝 y] g₂) :
  Prod.map f₁ g₁ =ᶠ[𝓝 (x, y)] Prod.map f₂ g₂

Full source

theorem Filter.EventuallyEq.prodMap_nhds {α β : Type*} {f₁ f₂ : X → α} {g₁ g₂ : Y → β}
    {x : X} {y : Y} (hf : f₁ =ᶠ[𝓝 x] f₂) (hg : g₁ =ᶠ[𝓝 y] g₂) :
    Prod.mapProd.map f₁ g₁ =ᶠ[𝓝 (x, y)] Prod.map f₂ g₂ := by
  rw [nhds_prod_eq]
  exact hf.prodMap hg

Eventual Equality of Product Maps in Neighborhood Filters

Informal description

Let $X$ and $Y$ be topological spaces, and let $\alpha$ and $\beta$ be types. For functions $f_1, f_2: X \to \alpha$ and $g_1, g_2: Y \to \beta$, and points $x \in X$ and $y \in Y$, if $f_1$ is eventually equal to $f_2$ in the neighborhood filter of $x$ and $g_1$ is eventually equal to $g_2$ in the neighborhood filter of $y$, then the product map $(f_1, g_1)$ is eventually equal to $(f_2, g_2)$ in the neighborhood filter of $(x, y)$ in the product space $X \times Y$. In symbols: \[ f_1 =_{\mathcal{N}(x)} f_2 \land g_1 =_{\mathcal{N}(y)} g_2 \implies (f_1, g_1) =_{\mathcal{N}(x, y)} (f_2, g_2) \] where $=_{\mathcal{N}(a)}$ denotes eventual equality in the neighborhood filter of $a$.

Filter.EventuallyLE.prodMap_nhds theorem

 {α β : Type*} [LE α] [LE β] {f₁ f₂ : X → α} {g₁ g₂ : Y → β} {x : X} {y : Y} (hf : f₁ ≤ᶠ[𝓝 x] f₂) (hg : g₁ ≤ᶠ[𝓝 y] g₂) :
  Prod.map f₁ g₁ ≤ᶠ[𝓝 (x, y)] Prod.map f₂ g₂

Full source

theorem Filter.EventuallyLE.prodMap_nhds {α β : Type*} [LE α] [LE β] {f₁ f₂ : X → α} {g₁ g₂ : Y → β}
    {x : X} {y : Y} (hf : f₁ ≤ᶠ[𝓝 x] f₂) (hg : g₁ ≤ᶠ[𝓝 y] g₂) :
    Prod.mapProd.map f₁ g₁ ≤ᶠ[𝓝 (x, y)] Prod.map f₂ g₂ := by
  rw [nhds_prod_eq]
  exact hf.prodMap hg

Eventual Inequality Preservation Under Product Mapping in Neighborhood Filters

Informal description

Let $X$ and $Y$ be topological spaces, and let $\alpha$ and $\beta$ be types equipped with preorders. For functions $f_1, f_2: X \to \alpha$ and $g_1, g_2: Y \to \beta$, and points $x \in X$, $y \in Y$, if $f_1 \leq f_2$ eventually near $x$ and $g_1 \leq g_2$ eventually near $y$, then the product map $(f_1, g_1) \leq (f_2, g_2)$ eventually near $(x, y)$ in the product space $X \times Y$. In symbols: \[ f_1 \leq_{\mathcal{N}(x)} f_2 \text{ and } g_1 \leq_{\mathcal{N}(y)} g_2 \implies (f_1, g_1) \leq_{\mathcal{N}(x,y)} (f_2, g_2) \] where $\leq_{\mathcal{N}(x)}$ denotes eventual inequality in the neighborhood filter at $x$, and similarly for other filters.

nhds_swap theorem

(x : X) (y : Y) : 𝓝 (x, y) = (𝓝 (y, x)).map Prod.swap

Full source

theorem nhds_swap (x : X) (y : Y) : 𝓝 (x, y) = (𝓝 (y, x)).map Prod.swap := by
  rw [nhds_prod_eq, Filter.prod_comm, nhds_prod_eq]; rfl

Neighborhood Filter of Product Space Under Swap

Informal description

For any topological spaces $X$ and $Y$, and any points $x \in X$ and $y \in Y$, the neighborhood filter of the point $(x, y)$ in the product space $X \times Y$ is equal to the image under the swap map of the neighborhood filter of $(y, x)$. In symbols: \[ \mathcal{N}(x, y) = \text{map}(\text{swap}, \mathcal{N}(y, x)) \] where $\mathcal{N}(x, y)$ denotes the neighborhood filter at $(x, y)$ in $X \times Y$, and $\text{swap} : Y \times X \to X \times Y$ is the function that swaps the components of a pair.

Filter.Tendsto.prodMk_nhds theorem

 {γ} {x : X} {y : Y} {f : Filter γ} {mx : γ → X} {my : γ → Y} (hx : Tendsto mx f (𝓝 x)) (hy : Tendsto my f (𝓝 y)) :
  Tendsto (fun c => (mx c, my c)) f (𝓝 (x, y))

Full source

theorem Filter.Tendsto.prodMk_nhds {γ} {x : X} {y : Y} {f : Filter γ} {mx : γ → X} {my : γ → Y}
    (hx : Tendsto mx f (𝓝 x)) (hy : Tendsto my f (𝓝 y)) :
    Tendsto (fun c => (mx c, my c)) f (𝓝 (x, y)) := by
  rw [nhds_prod_eq]
  exact hx.prodMk hy

Convergence of Product Map in Neighborhood Filters

Informal description

Let $X$ and $Y$ be topological spaces, $\gamma$ a type, and $f$ a filter on $\gamma$. For functions $m_x : \gamma \to X$ and $m_y : \gamma \to Y$, if $m_x$ tends to $x \in X$ along $f$ and $m_y$ tends to $y \in Y$ along $f$, then the product map $c \mapsto (m_x(c), m_y(c))$ tends to $(x, y)$ in the product space $X \times Y$ along $f$. In symbols: \[ m_x \underset{f}{\to} x \text{ and } m_y \underset{f}{\to} y \implies (m_x, m_y) \underset{f}{\to} (x, y) \] where $\underset{f}{\to}$ denotes convergence in the respective neighborhood filters.

Filter.Tendsto.prodMap_nhds theorem

 {x : X} {y : Y} {z : Z} {w : W} {f : X → Y} {g : Z → W} (hf : Tendsto f (𝓝 x) (𝓝 y)) (hg : Tendsto g (𝓝 z) (𝓝 w)) :
  Tendsto (Prod.map f g) (𝓝 (x, z)) (𝓝 (y, w))

Full source

theorem Filter.Tendsto.prodMap_nhds {x : X} {y : Y} {z : Z} {w : W} {f : X → Y} {g : Z → W}
    (hf : Tendsto f (𝓝 x) (𝓝 y)) (hg : Tendsto g (𝓝 z) (𝓝 w)) :
    Tendsto (Prod.map f g) (𝓝 (x, z)) (𝓝 (y, w)) := by
  rw [nhds_prod_eq, nhds_prod_eq]
  exact hf.prodMap hg

Continuity of Product Map under Pointwise Limits

Informal description

Let $X, Y, Z, W$ be topological spaces, and let $f : X \to Y$ and $g : Z \to W$ be functions. For any points $x \in X$, $y \in Y$, $z \in Z$, and $w \in W$, if $f$ tends to $y$ as $x'$ approaches $x$ and $g$ tends to $w$ as $z'$ approaches $z$, then the product map $f \times g : X \times Z \to Y \times W$ defined by $(f \times g)(x', z') = (f(x'), g(z'))$ tends to $(y, w)$ as $(x', z')$ approaches $(x, z)$. In symbols: \[ \lim_{x' \to x} f(x') = y \text{ and } \lim_{z' \to z} g(z') = w \implies \lim_{(x', z') \to (x, z)} (f(x'), g(z')) = (y, w). \]

Filter.Eventually.curry_nhds theorem

 {p : X × Y → Prop} {x : X} {y : Y} (h : ∀ᶠ x in 𝓝 (x, y), p x) : ∀ᶠ x' in 𝓝 x, ∀ᶠ y' in 𝓝 y, p (x', y')

Full source

theorem Filter.Eventually.curry_nhds {p : X × Y → Prop} {x : X} {y : Y}
    (h : ∀ᶠ x in 𝓝 (x, y), p x) : ∀ᶠ x' in 𝓝 x, ∀ᶠ y' in 𝓝 y, p (x', y') := by
  rw [nhds_prod_eq] at h
  exact h.curry

Neighborhood Property Factorization in Product Spaces

Informal description

For any topological spaces $X$ and $Y$, any point $(x, y) \in X \times Y$, and any property $p$ of $X \times Y$, if $p$ holds for all points in some neighborhood of $(x, y)$, then there exist neighborhoods $U$ of $x$ in $X$ and $V$ of $y$ in $Y$ such that $p(x', y')$ holds for all $(x', y') \in U \times V$. In symbols: \[ \left( \forall z \text{ near } (x, y), p(z) \right) \implies \left( \exists U \in \mathcal{N}(x), \exists V \in \mathcal{N}(y), \forall (x', y') \in U \times V, p(x', y') \right) \]

ContinuousAt.prodMk theorem

 {f : X → Y} {g : X → Z} {x : X} (hf : ContinuousAt f x) (hg : ContinuousAt g x) : ContinuousAt (fun x => (f x, g x)) x

Full source

@[fun_prop]
theorem ContinuousAt.prodMk {f : X → Y} {g : X → Z} {x : X} (hf : ContinuousAt f x)
    (hg : ContinuousAt g x) : ContinuousAt (fun x => (f x, g x)) x :=
  hf.prodMk_nhds hg

Continuity of Product Map at a Point

Informal description

Let $X$, $Y$, and $Z$ be topological spaces, and let $f \colon X \to Y$ and $g \colon X \to Z$ be functions. For a point $x \in X$, if $f$ is continuous at $x$ and $g$ is continuous at $x$, then the product map $x \mapsto (f(x), g(x))$ is continuous at $x$. In symbols: \[ \text{ContinuousAt } f \, x \text{ and } \text{ContinuousAt } g \, x \implies \text{ContinuousAt } (\lambda x \mapsto (f(x), g(x))) \, x. \]

ContinuousAt.prodMap theorem

 {f : X → Z} {g : Y → W} {p : X × Y} (hf : ContinuousAt f p.fst) (hg : ContinuousAt g p.snd) :
  ContinuousAt (Prod.map f g) p

Full source

theorem ContinuousAt.prodMap {f : X → Z} {g : Y → W} {p : X × Y} (hf : ContinuousAt f p.fst)
    (hg : ContinuousAt g p.snd) : ContinuousAt (Prod.map f g) p :=
  hf.fst''.prodMk hg.snd''

Continuity of Product Map at a Point in Product Spaces

Informal description

Let $X$, $Y$, $Z$, and $W$ be topological spaces, and let $f \colon X \to Z$ and $g \colon Y \to W$ be functions. For any point $p = (x, y) \in X \times Y$, if $f$ is continuous at $x$ and $g$ is continuous at $y$, then the product map $(f \times g) \colon X \times Y \to Z \times W$ defined by $(f \times g)(x, y) = (f(x), g(y))$ is continuous at $p$. In symbols: \[ \text{ContinuousAt } f \, x \text{ and } \text{ContinuousAt } g \, y \implies \text{ContinuousAt } (f \times g) \, (x, y). \]

ContinuousAt.prodMap' theorem

 {f : X → Z} {g : Y → W} {x : X} {y : Y} (hf : ContinuousAt f x) (hg : ContinuousAt g y) :
  ContinuousAt (Prod.map f g) (x, y)

Full source

/-- A version of `ContinuousAt.prodMap` that avoids `Prod.fst`/`Prod.snd`
by assuming that the point is `(x, y)`. -/
theorem ContinuousAt.prodMap' {f : X → Z} {g : Y → W} {x : X} {y : Y} (hf : ContinuousAt f x)
    (hg : ContinuousAt g y) : ContinuousAt (Prod.map f g) (x, y) :=
  hf.prodMap hg

Continuity of Product Map at a Point $(x, y)$ in Product Spaces

Informal description

Let $X$, $Y$, $Z$, and $W$ be topological spaces, and let $f \colon X \to Z$ and $g \colon Y \to W$ be functions. For any points $x \in X$ and $y \in Y$, if $f$ is continuous at $x$ and $g$ is continuous at $y$, then the product map $(f \times g) \colon X \times Y \to Z \times W$ defined by $(f \times g)(x, y) = (f(x), g(y))$ is continuous at the point $(x, y) \in X \times Y$. In symbols: \[ \text{ContinuousAt } f \, x \text{ and } \text{ContinuousAt } g \, y \implies \text{ContinuousAt } (f \times g) \, (x, y). \]

ContinuousAt.comp₂ theorem

 {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 ↦ f (g x, h x)) x

Full source

theorem ContinuousAt.comp₂ {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 ↦ f (g x, h x)) x :=
  ContinuousAt.comp hf (hg.prodMk hh)

Continuity of Binary Composition at a Point

Informal description

Let $X$, $Y$, $Z$, and $W$ be topological spaces, and let $f \colon Y \times Z \to W$, $g \colon X \to Y$, and $h \colon X \to Z$ be functions. For a point $x \in X$, if $f$ is continuous at $(g(x), h(x))$, $g$ is continuous at $x$, and $h$ is continuous at $x$, then the function $x \mapsto f(g(x), h(x))$ is continuous at $x$. In symbols: \[ \text{ContinuousAt } f \, (g(x), h(x)) \text{ and } \text{ContinuousAt } g \, x \text{ and } \text{ContinuousAt } h \, x \implies \text{ContinuousAt } (\lambda x \mapsto f(g(x), h(x))) \, x. \]

ContinuousAt.comp₂_of_eq theorem

 {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 ↦ f (g x, h x)) x

Full source

theorem ContinuousAt.comp₂_of_eq {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 ↦ f (g x, h x)) x := by
  rw [← e] at hf
  exact hf.comp₂ hg hh

Continuity of Binary Composition at a Point with Equality Condition

Informal description

Let $X$, $Y$, $Z$, and $W$ be topological spaces, and let $f \colon Y \times Z \to W$, $g \colon X \to Y$, and $h \colon X \to Z$ be functions. For a point $x \in X$ and $y \in Y \times Z$, if $f$ is continuous at $y$, $g$ is continuous at $x$, $h$ is continuous at $x$, and $(g(x), h(x)) = y$, then the function $x \mapsto f(g(x), h(x))$ is continuous at $x$. In symbols: \[ \text{ContinuousAt } f \, y \text{ and } \text{ContinuousAt } g \, x \text{ and } \text{ContinuousAt } h \, x \text{ and } (g(x), h(x)) = y \implies \text{ContinuousAt } (\lambda x \mapsto f(g(x), h(x))) \, x. \]

Continuous.curry_left theorem

{f : X × Y → Z} (hf : Continuous f) {y : Y} : Continuous fun x ↦ f (x, y)

Full source

/-- Continuous functions on products are continuous in their first argument -/
theorem Continuous.curry_left {f : X × Y → Z} (hf : Continuous f) {y : Y} :
    Continuous fun x ↦ f (x, y) :=
  hf.comp (.prodMk_left _)

Continuity of the Left Curry of a Continuous Function on Product Spaces

Informal description

Let $X$, $Y$, and $Z$ be topological spaces, and let $f \colon X \times Y \to Z$ be a continuous function. For any fixed $y \in Y$, the function $g \colon X \to Z$ defined by $g(x) = f(x, y)$ is continuous.

Continuous.curry_right theorem

{f : X × Y → Z} (hf : Continuous f) {x : X} : Continuous fun y ↦ f (x, y)

Full source

/-- Continuous functions on products are continuous in their second argument -/
theorem Continuous.curry_right {f : X × Y → Z} (hf : Continuous f) {x : X} :
    Continuous fun y ↦ f (x, y) :=
  hf.comp (.prodMk_right _)

Continuity of Partial Application in Second Variable

Informal description

Let $X$, $Y$, and $Z$ be topological spaces, and let $f \colon X \times Y \to Z$ be a continuous function. For any fixed $x \in X$, the function $g \colon Y \to Z$ defined by $g(y) = f(x, y)$ is continuous.

prod_generateFrom_generateFrom_eq theorem

 {X Y : Type*} {s : Set (Set X)} {t : Set (Set Y)} (hs : ⋃₀ s = univ) (ht : ⋃₀ t = univ) :
  @instTopologicalSpaceProd X Y (generateFrom s) (generateFrom t) = generateFrom (image2 (· ×ˢ ·) s t)

Full source

theorem prod_generateFrom_generateFrom_eq {X Y : Type*} {s : Set (Set X)} {t : Set (Set Y)}
    (hs : ⋃₀ s = univ) (ht : ⋃₀ t = univ) :
    @instTopologicalSpaceProd X Y (generateFrom s) (generateFrom t) =
      generateFrom (image2 (·  ×ˢ ·) s t) :=
  let G := generateFrom (image2  (·  ×ˢ ·) s t)
  le_antisymm
    (le_generateFrom fun _ ⟨_, hu, _, hv, g_eq⟩ =>
      g_eq.symm ▸
        @IsOpen.prod _ _ (generateFrom s) (generateFrom t) _ _ (GenerateOpen.basic _ hu)
          (GenerateOpen.basic _ hv))
    (le_inf
      (coinduced_le_iff_le_induced.mp <|
        le_generateFrom fun u hu =>
          have : ⋃ v ∈ t, u ×ˢ v = Prod.fstProd.fst ⁻¹' u := by
            simp_rw [← prod_iUnion, ← sUnion_eq_biUnion, ht, prod_univ]
          show G.IsOpen (Prod.fstProd.fst ⁻¹' u) by
            rw [← this]
            exact
              isOpen_iUnion fun v =>
                isOpen_iUnion fun hv => GenerateOpen.basic _ ⟨_, hu, _, hv, rfl⟩)
      (coinduced_le_iff_le_induced.mp <|
        le_generateFrom fun v hv =>
          have : ⋃ u ∈ s, u ×ˢ v = Prod.sndProd.snd ⁻¹' v := by
            simp_rw [← iUnion_prod_const, ← sUnion_eq_biUnion, hs, univ_prod]
          show G.IsOpen (Prod.sndProd.snd ⁻¹' v) by
            rw [← this]
            exact
              isOpen_iUnion fun u =>
                isOpen_iUnion fun hu => GenerateOpen.basic _ ⟨_, hu, _, hv, rfl⟩))

Product Topology as Generated by Products of Generating Sets

Informal description

Let $X$ and $Y$ be topological spaces with topologies generated by collections of sets $s \subseteq \mathcal{P}(X)$ and $t \subseteq \mathcal{P}(Y)$ respectively, where $\bigcup s = X$ and $\bigcup t = Y$. Then the product topology on $X \times Y$ is equal to the topology generated by the collection of all product sets $u \times v$ where $u \in s$ and $v \in t$.

prod_eq_generateFrom theorem

: instTopologicalSpaceProd = generateFrom {g | ∃ (s : Set X) (t : Set Y), IsOpen s ∧ IsOpen t ∧ g = s ×ˢ t}

Full source

theorem prod_eq_generateFrom :
    instTopologicalSpaceProd =
      generateFrom { g | ∃ (s : Set X) (t : Set Y), IsOpen s ∧ IsOpen t ∧ g = s ×ˢ t } :=
  le_antisymm (le_generateFrom fun _ ⟨_, _, hs, ht, g_eq⟩ => g_eq.symm ▸ hs.prod ht)
    (le_inf
      (forall_mem_image.2 fun t ht =>
        GenerateOpen.basic _ ⟨t, univ, by simpa [Set.prod_eq] using ht⟩)
      (forall_mem_image.2 fun t ht =>
        GenerateOpen.basic _ ⟨univ, t, by simpa [Set.prod_eq] using ht⟩))

Product Topology as Generated by Open Rectangles

Informal description

The product topology on $X \times Y$ is equal to the topology generated by the collection of all sets of the form $s \times t$, where $s$ is an open set in $X$ and $t$ is an open set in $Y$.

isOpen_prod_iff theorem

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

Full source

theorem isOpen_prod_iff {s : Set (X × Y)} :
    IsOpenIsOpen s ↔ ∀ a b, (a, b) ∈ s →
      ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ s :=
  isOpen_iff_mem_nhds.trans <| by simp_rw [Prod.forall, mem_nhds_prod_iff', and_left_comm]

Characterization of Open Sets in Product Topology

Informal description

A subset $s$ of the product space $X \times Y$ is open if and only if for every point $(a, b) \in s$, there exist open sets $u \subseteq X$ and $v \subseteq Y$ such that $a \in u$, $b \in v$, and the product set $u \times v$ is contained in $s$.

prod_induced_induced theorem

 {X Z} (f : X → Y) (g : Z → W) :
  @instTopologicalSpaceProd X Z (induced f ‹_›) (induced g ‹_›) =
    induced (fun p => (f p.1, g p.2)) instTopologicalSpaceProd

Full source

/-- A product of induced topologies is induced by the product map -/
theorem prod_induced_induced {X Z} (f : X → Y) (g : Z → W) :
    @instTopologicalSpaceProd X Z (induced f ‹_›) (induced g ‹_›) =
      induced (fun p => (f p.1, g p.2)) instTopologicalSpaceProd := by
  delta instTopologicalSpaceProd
  simp_rw [induced_inf, induced_compose]
  rfl

Product of Induced Topologies Equals Induced Product Topology

Informal description

Let $X$ and $Z$ be types with topologies induced by functions $f \colon X \to Y$ and $g \colon Z \to W$ respectively. Then the product topology on $X \times Z$ induced by these topologies is equal to the topology induced on $X \times Z$ by the product map $(f \times g) \colon X \times Z \to Y \times W$ defined by $(x,z) \mapsto (f(x), g(z))$ from the product topology on $Y \times W$.

exists_nhds_square theorem

{s : Set (X × X)} {x : X} (hx : s ∈ 𝓝 (x, x)) : ∃ U : Set X, IsOpen U ∧ x ∈ U ∧ U ×ˢ U ⊆ s

Full source

/-- Given a neighborhood `s` of `(x, x)`, then `(x, x)` has a square open neighborhood
  that is a subset of `s`. -/
theorem exists_nhds_square {s : Set (X × X)} {x : X} (hx : s ∈ 𝓝 (x, x)) :
    ∃ U : Set X, IsOpen U ∧ x ∈ U ∧ U ×ˢ U ⊆ s := by
  simpa [nhds_prod_eq, (nhds_basis_opens x).prod_self.mem_iff, and_assoc, and_left_comm] using hx

Existence of Square Neighborhood in Product Space

Informal description

For any topological space $X$, given a neighborhood $s$ of the point $(x, x)$ in $X \times X$, there exists an open set $U \subseteq X$ containing $x$ such that the product set $U \times U$ is contained in $s$.

map_fst_nhdsWithin theorem

(x : X × Y) : map Prod.fst (𝓝[Prod.snd ⁻¹' { x.2 }] x) = 𝓝 x.1

Full source

/-- `Prod.fst` maps neighborhood of `x : X × Y` within the section `Prod.snd ⁻¹' {x.2}`
to `𝓝 x.1`. -/
theorem map_fst_nhdsWithin (x : X × Y) : map Prod.fst (𝓝[Prod.snd ⁻¹' {x.2}] x) = 𝓝 x.1 := by
  refine le_antisymm (continuousAt_fst.mono_left inf_le_left) fun s hs => ?_
  rcases x with ⟨x, y⟩
  rw [mem_map, nhdsWithin, mem_inf_principal, mem_nhds_prod_iff] at hs
  rcases hs with ⟨u, hu, v, hv, H⟩
  simp only [prod_subset_iff, mem_singleton_iff, mem_setOf_eq, mem_preimage] at H
  exact mem_of_superset hu fun z hz => H _ hz _ (mem_of_mem_nhds hv) rfl

First Projection Maps Vertical Section Neighborhood Filter to Base Space Neighborhood Filter

Informal description

For any point $x = (x_1, x_2)$ in the product space $X \times Y$, the image under the first projection $\pi_1$ of the neighborhood filter of $x$ restricted to the vertical section $\pi_2^{-1}(\{x_2\})$ equals the neighborhood filter of $x_1$ in $X$. In symbols: \[ \pi_1_*(\mathcal{N}_{\pi_2^{-1}(\{x_2\})}(x)) = \mathcal{N}(x_1) \] where $\mathcal{N}_{\pi_2^{-1}(\{x_2\})}(x)$ denotes the neighborhood filter of $x$ within the vertical section $\pi_2^{-1}(\{x_2\})$, and $\mathcal{N}(x_1)$ is the neighborhood filter of $x_1$ in $X$.

map_fst_nhds theorem

(x : X × Y) : map Prod.fst (𝓝 x) = 𝓝 x.1

Full source

@[simp]
theorem map_fst_nhds (x : X × Y) : map Prod.fst (𝓝 x) = 𝓝 x.1 :=
  le_antisymm continuousAt_fst <| (map_fst_nhdsWithin x).symm.trans_le (map_mono inf_le_left)

First Projection Preserves Neighborhood Filters in Product Space

Informal description

For any point $x = (x_1, x_2)$ in the product topological space $X \times Y$, the image under the first projection $\pi_1 \colon X \times Y \to X$ of the neighborhood filter $\mathcal{N}(x)$ equals the neighborhood filter $\mathcal{N}(x_1)$ of $x_1$ in $X$. In symbols: \[ (\pi_1)_*(\mathcal{N}(x)) = \mathcal{N}(x_1) \]

isOpenMap_fst theorem

: IsOpenMap (@Prod.fst X Y)

Full source

/-- The first projection in a product of topological spaces sends open sets to open sets. -/
theorem isOpenMap_fst : IsOpenMap (@Prod.fst X Y) :=
  isOpenMap_iff_nhds_le.2 fun x => (map_fst_nhds x).ge

First Projection is an Open Map in Product Topology

Informal description

The first projection map $\pi_1 \colon X \times Y \to X$ from the product topological space $X \times Y$ to $X$ is an open map. That is, for every open subset $U \subseteq X \times Y$, the image $\pi_1(U)$ is open in $X$.

map_snd_nhdsWithin theorem

(x : X × Y) : map Prod.snd (𝓝[Prod.fst ⁻¹' { x.1 }] x) = 𝓝 x.2

Full source

/-- `Prod.snd` maps neighborhood of `x : X × Y` within the section `Prod.fst ⁻¹' {x.1}`
to `𝓝 x.2`. -/
theorem map_snd_nhdsWithin (x : X × Y) : map Prod.snd (𝓝[Prod.fst ⁻¹' {x.1}] x) = 𝓝 x.2 := by
  refine le_antisymm (continuousAt_snd.mono_left inf_le_left) fun s hs => ?_
  rcases x with ⟨x, y⟩
  rw [mem_map, nhdsWithin, mem_inf_principal, mem_nhds_prod_iff] at hs
  rcases hs with ⟨u, hu, v, hv, H⟩
  simp only [prod_subset_iff, mem_singleton_iff, mem_setOf_eq, mem_preimage] at H
  exact mem_of_superset hv fun z hz => H _ (mem_of_mem_nhds hu) _ hz rfl

Second Projection Maps Vertical Section Neighborhoods to Point Neighborhoods in Product Space

Informal description

For any point $x = (x_1, x_2)$ in the product topological space $X \times Y$, the image under the second projection map $\text{snd} \colon X \times Y \to Y$ of the neighborhood filter of $x$ restricted to the vertical section $\text{fst}^{-1}(\{x_1\})$ equals the neighborhood filter of $x_2$ in $Y$. In symbols: \[ \text{snd}_*(\mathcal{N}_{\text{fst}^{-1}(\{x_1\})}(x)) = \mathcal{N}(x_2) \] where $\mathcal{N}_{\text{fst}^{-1}(\{x_1\})}(x)$ denotes the neighborhood filter of $x$ within the vertical section $\text{fst}^{-1}(\{x_1\})$, and $\mathcal{N}(x_2)$ is the neighborhood filter of $x_2$ in $Y$.

map_snd_nhds theorem

(x : X × Y) : map Prod.snd (𝓝 x) = 𝓝 x.2

Full source

@[simp]
theorem map_snd_nhds (x : X × Y) : map Prod.snd (𝓝 x) = 𝓝 x.2 :=
  le_antisymm continuousAt_snd <| (map_snd_nhdsWithin x).symm.trans_le (map_mono inf_le_left)

Second Projection Preserves Neighborhood Filters in Product Space

Informal description

For any point $x = (x_1, x_2)$ in the product topological space $X \times Y$, the image under the second projection map $\text{snd} \colon X \times Y \to Y$ of the neighborhood filter of $x$ equals the neighborhood filter of $x_2$ in $Y$. In symbols: \[ \text{snd}_*(\mathcal{N}(x)) = \mathcal{N}(x_2) \] where $\mathcal{N}(x)$ denotes the neighborhood filter of $x$ in $X \times Y$, and $\mathcal{N}(x_2)$ is the neighborhood filter of $x_2$ in $Y$.

isOpenMap_snd theorem

: IsOpenMap (@Prod.snd X Y)

Full source

/-- The second projection in a product of topological spaces sends open sets to open sets. -/
theorem isOpenMap_snd : IsOpenMap (@Prod.snd X Y) :=
  isOpenMap_iff_nhds_le.2 fun x => (map_snd_nhds x).ge

Second Projection is an Open Map in Product Spaces

Informal description

The second projection map $\text{snd} \colon X \times Y \to Y$ from the product topological space $X \times Y$ to $Y$ is an open map. That is, for every open subset $U \subseteq X \times Y$, the image $\text{snd}(U)$ is open in $Y$.

isOpen_prod_iff' theorem

{s : Set X} {t : Set Y} : IsOpen (s ×ˢ t) ↔ IsOpen s ∧ IsOpen t ∨ s = ∅ ∨ t = ∅

Full source

/-- A product set is open in a product space if and only if each factor is open, or one of them is
empty -/
theorem isOpen_prod_iff' {s : Set X} {t : Set Y} :
    IsOpenIsOpen (s ×ˢ t) ↔ IsOpen s ∧ IsOpen t ∨ s = ∅ ∨ t = ∅ := by
  rcases (s ×ˢ t).eq_empty_or_nonempty with h | h
  · simp [h, prod_eq_empty_iff.1 h]
  · have st : s.Nonempty ∧ t.Nonempty := prod_nonempty_iff.1 h
    constructor
    · intro (H : IsOpen (s ×ˢ t))
      refine Or.inl ⟨?_, ?_⟩
      · simpa only [fst_image_prod _ st.2] using isOpenMap_fst _ H
      · simpa only [snd_image_prod st.1 t] using isOpenMap_snd _ H
    · intro H
      simp only [st.1.ne_empty, st.2.ne_empty, not_false_iff, or_false] at H
      exact H.1.prod H.2

Openness Condition for Product Sets: $\text{IsOpen}(s \times t) \leftrightarrow (\text{IsOpen}(s) \land \text{IsOpen}(t)) \lor s = \emptyset \lor t = \emptyset$

Informal description

For any subsets $s \subseteq X$ and $t \subseteq Y$ of topological spaces $X$ and $Y$, the product set $s \times t$ is open in the product space $X \times Y$ if and only if either both $s$ and $t$ are open in their respective spaces, or at least one of them is empty. In other words: \[ \text{IsOpen}(s \times t) \leftrightarrow (\text{IsOpen}(s) \land \text{IsOpen}(t)) \lor s = \emptyset \lor t = \emptyset. \]

isQuotientMap_fst theorem

[Nonempty Y] : IsQuotientMap (Prod.fst : X × Y → X)

Full source

theorem isQuotientMap_fst [Nonempty Y] : IsQuotientMap (Prod.fst : X × Y → X) :=
  isOpenMap_fst.isQuotientMap continuous_fst Prod.fst_surjective

First Projection is a Quotient Map for Nonempty $Y$

Informal description

For any nonempty topological space $Y$, the first projection map $\pi_1 \colon X \times Y \to X$ is a quotient map. That is, $\pi_1$ is continuous, surjective, and a subset $U \subseteq X$ is open if and only if its preimage $\pi_1^{-1}(U)$ is open in $X \times Y$.

isQuotientMap_snd theorem

[Nonempty X] : IsQuotientMap (Prod.snd : X × Y → Y)

Full source

theorem isQuotientMap_snd [Nonempty X] : IsQuotientMap (Prod.snd : X × Y → Y) :=
  isOpenMap_snd.isQuotientMap continuous_snd Prod.snd_surjective

Second Projection is a Quotient Map for Nonempty Spaces

Informal description

For nonempty topological spaces $X$ and $Y$, the second projection map $\operatorname{snd} \colon X \times Y \to Y$ is a quotient map. That is, $\operatorname{snd}$ is surjective and a subset $U \subseteq Y$ is open if and only if its preimage $\operatorname{snd}^{-1}(U)$ is open in $X \times Y$.

closure_prod_eq theorem

{s : Set X} {t : Set Y} : closure (s ×ˢ t) = closure s ×ˢ closure t

Full source

theorem closure_prod_eq {s : Set X} {t : Set Y} : closure (s ×ˢ t) = closure s ×ˢ closure t :=
  ext fun ⟨a, b⟩ => by
    simp_rw [mem_prod, mem_closure_iff_nhdsWithin_neBot, nhdsWithin_prod_eq, prod_neBot]

Closure of Product Set Equals Product of Closures

Informal description

For any subsets $s \subseteq X$ and $t \subseteq Y$ of topological spaces $X$ and $Y$, the closure of the product set $s \times t$ in the product space $X \times Y$ is equal to the product of the closures of $s$ and $t$, i.e., \[ \overline{s \times t} = \overline{s} \times \overline{t}. \]

interior_prod_eq theorem

(s : Set X) (t : Set Y) : interior (s ×ˢ t) = interior s ×ˢ interior t

Full source

theorem interior_prod_eq (s : Set X) (t : Set Y) : interior (s ×ˢ t) = interior s ×ˢ interior t :=
  ext fun ⟨a, b⟩ => by simp only [mem_interior_iff_mem_nhds, mem_prod, prod_mem_nhds_iff]

Interior of Product Set Equals Product of Interiors

Informal description

For any subsets $s \subseteq X$ and $t \subseteq Y$ of topological spaces $X$ and $Y$, the interior of the product set $s \times t$ in the product space $X \times Y$ is equal to the product of the interiors of $s$ and $t$, i.e., \[ \text{interior}(s \times t) = \text{interior}(s) \times \text{interior}(t). \]

frontier_prod_eq theorem

(s : Set X) (t : Set Y) : frontier (s ×ˢ t) = closure s ×ˢ frontier t ∪ frontier s ×ˢ closure t

Full source

theorem frontier_prod_eq (s : Set X) (t : Set Y) :
    frontier (s ×ˢ t) = closureclosure s ×ˢ frontier t ∪ frontier s ×ˢ closure t := by
  simp only [frontier, closure_prod_eq, interior_prod_eq, prod_diff_prod]

Frontier of Product Set Decomposition

Informal description

For any subsets $s \subseteq X$ and $t \subseteq Y$ of topological spaces $X$ and $Y$, the frontier of the product set $s \times t$ in the product space $X \times Y$ is equal to the union of: 1. the product of the closure of $s$ with the frontier of $t$, and 2. the product of the frontier of $s$ with the closure of $t$. In other words: $$\text{frontier}(s \times t) = (\overline{s} \times \text{frontier}(t)) \cup (\text{frontier}(s) \times \overline{t})$$

frontier_prod_univ_eq theorem

(s : Set X) : frontier (s ×ˢ (univ : Set Y)) = frontier s ×ˢ univ

Full source

@[simp]
theorem frontier_prod_univ_eq (s : Set X) :
    frontier (s ×ˢ (univ : Set Y)) = frontier s ×ˢ univ := by
  simp [frontier_prod_eq]

Frontier of Product with Universal Set Decomposition: $\text{frontier}(s \times Y) = \text{frontier}(s) \times Y$

Informal description

For any subset $s$ of a topological space $X$, the frontier of the product set $s \times Y$ in the product space $X \times Y$ is equal to the product of the frontier of $s$ with the universal set $Y$, i.e., \[ \text{frontier}(s \times Y) = \text{frontier}(s) \times Y. \]

frontier_univ_prod_eq theorem

(s : Set Y) : frontier ((univ : Set X) ×ˢ s) = univ ×ˢ frontier s

Full source

@[simp]
theorem frontier_univ_prod_eq (s : Set Y) :
    frontier ((univ : Set X) ×ˢ s) = univ ×ˢ frontier s := by
  simp [frontier_prod_eq]

Frontier of Universal Product Set Decomposition: $\text{frontier}(X \times s) = X \times \text{frontier}(s)$

Informal description

For any subset $s$ of a topological space $Y$, the frontier of the product set $X \times s$ in the product space $X \times Y$ is equal to the product of the universal set $X$ with the frontier of $s$. In other words: $$\text{frontier}(X \times s) = X \times \text{frontier}(s)$$

map_mem_closure₂ theorem

 {f : X → Y → Z} {x : X} {y : Y} {s : Set X} {t : Set Y} {u : Set Z} (hf : Continuous (uncurry f)) (hx : x ∈ closure s)
  (hy : y ∈ closure t) (h : ∀ a ∈ s, ∀ b ∈ t, f a b ∈ u) : f x y ∈ closure u

Full source

theorem map_mem_closure₂ {f : X → Y → Z} {x : X} {y : Y} {s : Set X} {t : Set Y} {u : Set Z}
    (hf : Continuous (uncurry f)) (hx : x ∈ closure s) (hy : y ∈ closure t)
    (h : ∀ a ∈ s, ∀ b ∈ t, f a b ∈ u) : f x y ∈ closure u :=
  have H₁ : (x, y)(x, y) ∈ closure (s ×ˢ t) := by simpa only [closure_prod_eq] using mk_mem_prod hx hy
  have H₂ : MapsTo (uncurry f) (s ×ˢ t) u := forall_prod_set.2 h
  H₂.closure hf H₁

Continuous Functions Preserve Closure Under Binary Mapping

Informal description

Let $X$, $Y$, and $Z$ be topological spaces, and let $f \colon X \to Y \to Z$ be a continuous function (with respect to the product topology on $X \times Y$). Suppose $x \in \overline{s}$ and $y \in \overline{t}$ for subsets $s \subseteq X$ and $t \subseteq Y$. If for every $a \in s$ and $b \in t$, the image $f(a, b)$ belongs to a subset $u \subseteq Z$, then $f(x, y) \in \overline{u}$.

IsClosed.prod theorem

{s₁ : Set X} {s₂ : Set Y} (h₁ : IsClosed s₁) (h₂ : IsClosed s₂) : IsClosed (s₁ ×ˢ s₂)

Full source

theorem IsClosed.prod {s₁ : Set X} {s₂ : Set Y} (h₁ : IsClosed s₁) (h₂ : IsClosed s₂) :
    IsClosed (s₁ ×ˢ s₂) :=
  closure_eq_iff_isClosed.mp <| by simp only [h₁.closure_eq, h₂.closure_eq, closure_prod_eq]

Product of Closed Sets is Closed in Product Topology

Informal description

For any closed subsets $s_1 \subseteq X$ and $s_2 \subseteq Y$ of topological spaces $X$ and $Y$, the product set $s_1 \times s_2$ is closed in the product space $X \times Y$.

Dense.prod theorem

{s : Set X} {t : Set Y} (hs : Dense s) (ht : Dense t) : Dense (s ×ˢ t)

Full source

/-- The product of two dense sets is a dense set. -/
theorem Dense.prod {s : Set X} {t : Set Y} (hs : Dense s) (ht : Dense t) : Dense (s ×ˢ t) :=
  fun x => by
  rw [closure_prod_eq]
  exact ⟨hs x.1, ht x.2⟩

Density of Product Sets in Product Spaces

Informal description

For any dense subsets $s \subseteq X$ and $t \subseteq Y$ of topological spaces $X$ and $Y$, the product set $s \times t$ is dense in the product space $X \times Y$.

DenseRange.prodMap theorem

 {ι : Type*} {κ : Type*} {f : ι → Y} {g : κ → Z} (hf : DenseRange f) (hg : DenseRange g) : DenseRange (Prod.map f g)

Full source

/-- If `f` and `g` are maps with dense range, then `Prod.map f g` has dense range. -/
theorem DenseRange.prodMap {ι : Type*} {κ : Type*} {f : ι → Y} {g : κ → Z} (hf : DenseRange f)
    (hg : DenseRange g) : DenseRange (Prod.map f g) := by
  simpa only [DenseRange, prod_range_range_eq] using hf.prod hg

Density of Product Map for Functions with Dense Ranges

Informal description

Let $f \colon \iota \to Y$ and $g \colon \kappa \to Z$ be functions between topological spaces with dense ranges. Then the product map $f \times g \colon \iota \times \kappa \to Y \times Z$ defined by $(x, y) \mapsto (f(x), g(y))$ also has dense range.

Topology.IsInducing.prodMap theorem

{f : X → Y} {g : Z → W} (hf : IsInducing f) (hg : IsInducing g) : IsInducing (Prod.map f g)

Full source

lemma Topology.IsInducing.prodMap {f : X → Y} {g : Z → W} (hf : IsInducing f) (hg : IsInducing g) :
    IsInducing (Prod.map f g) :=
  isInducing_iff_nhds.2 fun (x, z) => by simp_rw [Prod.map_def, nhds_prod_eq, hf.nhds_eq_comap,
    hg.nhds_eq_comap, prod_comap_comap_eq]

Product of Inducing Maps is Inducing

Informal description

Let $f \colon X \to Y$ and $g \colon Z \to W$ be inducing maps between topological spaces. Then the product map $f \times g \colon X \times Z \to Y \times W$ defined by $(x,z) \mapsto (f(x), g(z))$ is also inducing.

Topology.isInducing_const_prod theorem

{x : X} {f : Y → Z} : IsInducing (fun x' => (x, f x')) ↔ IsInducing f

Full source

@[simp]
lemma Topology.isInducing_const_prod {x : X} {f : Y → Z} :
    IsInducingIsInducing (fun x' => (x, f x')) ↔ IsInducing f := by
  simp_rw [isInducing_iff, instTopologicalSpaceProd, induced_inf, induced_compose,
    Function.comp_def, induced_const, top_inf_eq]

Inducing Property of Constant Product Map: $(x, f(-))$ is Inducing iff $f$ is Inducing

Informal description

For a fixed point $x \in X$ and a function $f \colon Y \to Z$, the map $Y \to X \times Z$ defined by $y \mapsto (x, f(y))$ is inducing (i.e., the topology on $Y$ is the coarsest making this map continuous) if and only if $f$ itself is inducing.

Topology.isInducing_prod_const theorem

{y : Y} {f : X → Z} : IsInducing (fun x => (f x, y)) ↔ IsInducing f

Full source

@[simp]
lemma Topology.isInducing_prod_const {y : Y} {f : X → Z} :
    IsInducingIsInducing (fun x => (f x, y)) ↔ IsInducing f := by
  simp_rw [isInducing_iff, instTopologicalSpaceProd, induced_inf, induced_compose,
    Function.comp_def, induced_const, inf_top_eq]

Inducing Property of Product with Constant Function

Informal description

For a fixed element $y \in Y$ and a function $f \colon X \to Z$, the map $x \mapsto (f(x), y)$ is inducing (i.e., the topology on $X$ is induced by this map) if and only if $f$ itself is inducing.

Topology.IsEmbedding.prodMap theorem

{f : X → Y} {g : Z → W} (hf : IsEmbedding f) (hg : IsEmbedding g) : IsEmbedding (Prod.map f g)

Full source

lemma Topology.IsEmbedding.prodMap {f : X → Y} {g : Z → W} (hf : IsEmbedding f)
    (hg : IsEmbedding g) : IsEmbedding (Prod.map f g) where
  toIsInducing := hf.isInducing.prodMap hg.isInducing
  injective := hf.injective.prodMap hg.injective

Product of Embeddings is an Embedding

Informal description

Let $f \colon X \to Y$ and $g \colon Z \to W$ be topological embeddings between topological spaces. Then the product map $f \times g \colon X \times Z \to Y \times W$ defined by $(x,z) \mapsto (f(x), g(z))$ is also a topological embedding.

IsOpenMap.prodMap theorem

{f : X → Y} {g : Z → W} (hf : IsOpenMap f) (hg : IsOpenMap g) : IsOpenMap (Prod.map f g)

Full source

protected theorem IsOpenMap.prodMap {f : X → Y} {g : Z → W} (hf : IsOpenMap f) (hg : IsOpenMap g) :
    IsOpenMap (Prod.map f g) := by
  rw [isOpenMap_iff_nhds_le]
  rintro ⟨a, b⟩
  rw [nhds_prod_eq, nhds_prod_eq, ← Filter.prod_map_map_eq']
  exact Filter.prod_mono (hf.nhds_le a) (hg.nhds_le b)

Product of Open Maps is Open

Informal description

Let $f \colon X \to Y$ and $g \colon Z \to W$ be open maps between topological spaces. Then the product map $f \times g \colon X \times Z \to Y \times W$ defined by $(x,z) \mapsto (f(x), g(z))$ is also an open map.

Topology.IsOpenEmbedding.prodMap theorem

{f : X → Y} {g : Z → W} (hf : IsOpenEmbedding f) (hg : IsOpenEmbedding g) : IsOpenEmbedding (Prod.map f g)

Full source

protected lemma Topology.IsOpenEmbedding.prodMap {f : X → Y} {g : Z → W} (hf : IsOpenEmbedding f)
    (hg : IsOpenEmbedding g) : IsOpenEmbedding (Prod.map f g) :=
  .of_isEmbedding_isOpenMap (hf.1.prodMap hg.1) (hf.isOpenMap.prodMap hg.isOpenMap)

Product of Open Embeddings is an Open Embedding

Informal description

Let $f \colon X \to Y$ and $g \colon Z \to W$ be open embeddings between topological spaces. Then the product map $f \times g \colon X \times Z \to Y \times W$ defined by $(x,z) \mapsto (f(x), g(z))$ is also an open embedding.

isEmbedding_graph theorem

{f : X → Y} (hf : Continuous f) : IsEmbedding fun x => (x, f x)

Full source

lemma isEmbedding_graph {f : X → Y} (hf : Continuous f) : IsEmbedding fun x => (x, f x) :=
  .of_comp (continuous_id.prodMk hf) continuous_fst .id

Graph of Continuous Function is Embedding

Informal description

For any continuous function $f \colon X \to Y$ between topological spaces, the graph map $x \mapsto (x, f(x))$ is a topological embedding of $X$ into $X \times Y$.

isEmbedding_prodMk theorem

(x : X) : IsEmbedding (Prod.mk x : Y → X × Y)

Full source

lemma isEmbedding_prodMk (x : X) : IsEmbedding (Prod.mk x : Y → X × Y) :=
  .of_comp (.prodMk_right x) continuous_snd .id

Embedding Property of Fixed-First-Coordinate Product Map

Informal description

For any topological spaces $X$ and $Y$, and any fixed element $x \in X$, the function $f \colon Y \to X \times Y$ defined by $f(y) = (x, y)$ is a topological embedding.

IsOpenQuotientMap.prodMap theorem

{f : X → Y} {g : Z → W} (hf : IsOpenQuotientMap f) (hg : IsOpenQuotientMap g) : IsOpenQuotientMap (Prod.map f g)

Full source

theorem IsOpenQuotientMap.prodMap {f : X → Y} {g : Z → W} (hf : IsOpenQuotientMap f)
    (hg : IsOpenQuotientMap g) : IsOpenQuotientMap (Prod.map f g) :=
  ⟨.prodMap hf.1 hg.1, .prodMap hf.2 hg.2, .prodMap hf.3 hg.3⟩

Product of Open Quotient Maps is Open Quotient Map

Informal description

Let $f \colon X \to Y$ and $g \colon Z \to W$ be open quotient maps between topological spaces. Then the product map $f \times g \colon X \times Z \to Y \times W$ defined by $(x,z) \mapsto (f(x), g(z))$ is also an open quotient map.

continuous_sum_dom theorem

{f : X ⊕ Y → Z} : Continuous f ↔ Continuous (f ∘ Sum.inl) ∧ Continuous (f ∘ Sum.inr)

Full source

theorem continuous_sum_dom {f : X ⊕ Y → Z} :
    ContinuousContinuous f ↔ Continuous (f ∘ Sum.inl) ∧ Continuous (f ∘ Sum.inr) :=
  (continuous_sup_dom (t₁ := TopologicalSpace.coinduced Sum.inl _)
    (t₂ := TopologicalSpace.coinduced Sum.inr _)).trans <|
    continuous_coinduced_dom.and continuous_coinduced_dom

Continuity Criterion for Functions on Disjoint Unions

Informal description

A function $f \colon X \oplus Y \to Z$ between topological spaces is continuous if and only if the compositions $f \circ \iota_X$ and $f \circ \iota_Y$ are continuous, where $\iota_X \colon X \to X \oplus Y$ and $\iota_Y \colon Y \to X \oplus Y$ are the canonical inclusion maps.

continuous_sumElim theorem

{f : X → Z} {g : Y → Z} : Continuous (Sum.elim f g) ↔ Continuous f ∧ Continuous g

Full source

theorem continuous_sumElim {f : X → Z} {g : Y → Z} :
    ContinuousContinuous (Sum.elim f g) ↔ Continuous f ∧ Continuous g :=
  continuous_sum_dom

Continuity of Eliminator Function on Disjoint Union

Informal description

For any topological spaces $X$, $Y$, and $Z$, the function $\text{Sum.elim}\, f\, g \colon X \oplus Y \to Z$ is continuous if and only if both $f \colon X \to Z$ and $g \colon Y \to Z$ are continuous.

Continuous.sumElim theorem

{f : X → Z} {g : Y → Z} (hf : Continuous f) (hg : Continuous g) : Continuous (Sum.elim f g)

Full source

@[continuity, fun_prop]
theorem Continuous.sumElim {f : X → Z} {g : Y → Z} (hf : Continuous f) (hg : Continuous g) :
    Continuous (Sum.elim f g) :=
  continuous_sumElim.2 ⟨hf, hg⟩

Continuity of the Eliminator Function on Disjoint Unions

Informal description

For any topological spaces $X$, $Y$, and $Z$, if $f \colon X \to Z$ and $g \colon Y \to Z$ are continuous functions, then the function $\text{Sum.elim}\, f\, g \colon X \oplus Y \to Z$ is also continuous.

continuous_isLeft theorem

: Continuous (isLeft : X ⊕ Y → Bool)

Full source

@[continuity, fun_prop]
theorem continuous_isLeft : Continuous (isLeft : X ⊕ Y → Bool) :=
  continuous_sum_dom.2 ⟨continuous_const, continuous_const⟩

Continuity of the Left Component Check Function on Disjoint Unions

Informal description

The function $\text{isLeft} \colon X \oplus Y \to \text{Bool}$, which checks whether an element of the disjoint union $X \oplus Y$ is in the left component $X$, is continuous with respect to the canonical topologies on $X \oplus Y$ and $\text{Bool}$.

continuous_isRight theorem

: Continuous (isRight : X ⊕ Y → Bool)

Full source

@[continuity, fun_prop]
theorem continuous_isRight : Continuous (isRight : X ⊕ Y → Bool) :=
  continuous_sum_dom.2 ⟨continuous_const, continuous_const⟩

Continuity of the Right Summand Check Function

Informal description

The function $\text{isRight} \colon X \oplus Y \to \text{Bool}$, which checks whether an element of the disjoint union $X \oplus Y$ is in the right summand $Y$, is continuous with respect to the canonical topologies on $X \oplus Y$ and $\text{Bool}$.

continuous_inl theorem

: Continuous (@inl X Y)

Full source

@[continuity, fun_prop]
theorem continuous_inl : Continuous (@inl X Y) := ⟨fun _ => And.left⟩

Continuity of Left Inclusion in Disjoint Union

Informal description

The inclusion map $\text{inl} \colon X \to X \oplus Y$ from a topological space $X$ into the disjoint union $X \oplus Y$ is continuous.

continuous_inr theorem

: Continuous (@inr X Y)

Full source

@[continuity, fun_prop]
theorem continuous_inr : Continuous (@inr X Y) := ⟨fun _ => And.right⟩

Continuity of the Right Inclusion into Disjoint Union

Informal description

The right inclusion map $\text{inr} \colon Y \to X \oplus Y$ from a topological space $Y$ into the disjoint union $X \oplus Y$ is continuous.

continuous_sum_swap theorem

: Continuous (@Sum.swap X Y)

Full source

@[fun_prop, continuity]
lemma continuous_sum_swap : Continuous (@Sum.swap X Y) :=
  Continuous.sumElim continuous_inr continuous_inl

Continuity of the Swap Function on Disjoint Unions

Informal description

The swap function $\text{Sum.swap} \colon X \oplus Y \to Y \oplus X$ between the disjoint unions of topological spaces is continuous.

isOpen_sum_iff theorem

{s : Set (X ⊕ Y)} : IsOpen s ↔ IsOpen (inl ⁻¹' s) ∧ IsOpen (inr ⁻¹' s)

Full source

theorem isOpen_sum_iff {s : Set (X ⊕ Y)} : IsOpenIsOpen s ↔ IsOpen (inl ⁻¹' s) ∧ IsOpen (inr ⁻¹' s) :=
  Iff.rfl

Characterization of Open Sets in Disjoint Union Topology

Informal description

A subset $s$ of the disjoint union $X \oplus Y$ of topological spaces is open if and only if its preimages under both the left inclusion $\text{inl} \colon X \to X \oplus Y$ and the right inclusion $\text{inr} \colon Y \to X \oplus Y$ are open in $X$ and $Y$ respectively.

isClosed_sum_iff theorem

{s : Set (X ⊕ Y)} : IsClosed s ↔ IsClosed (inl ⁻¹' s) ∧ IsClosed (inr ⁻¹' s)

Full source

theorem isClosed_sum_iff {s : Set (X ⊕ Y)} :
    IsClosedIsClosed s ↔ IsClosed (inl ⁻¹' s) ∧ IsClosed (inr ⁻¹' s) := by
  simp only [← isOpen_compl_iff, isOpen_sum_iff, preimage_compl]

Characterization of Closed Sets in Disjoint Union Topology

Informal description

A subset $s$ of the disjoint union $X \oplus Y$ of topological spaces is closed if and only if its preimages under both the left inclusion $\mathrm{inl} : X \to X \oplus Y$ and the right inclusion $\mathrm{inr} : Y \to X \oplus Y$ are closed in $X$ and $Y$ respectively.

isOpenMap_inl theorem

: IsOpenMap (@inl X Y)

Full source

theorem isOpenMap_inl : IsOpenMap (@inl X Y) := fun u hu => by
  simpa [isOpen_sum_iff, preimage_image_eq u Sum.inl_injective]

Left Inclusion is an Open Map for Disjoint Union Topology

Informal description

The left inclusion map $\mathrm{inl} \colon X \to X \oplus Y$ is an open map, meaning that for every open subset $U \subseteq X$, the image $\mathrm{inl}(U)$ is open in the disjoint union $X \oplus Y$ equipped with the sum topology.

isOpenMap_inr theorem

: IsOpenMap (@inr X Y)

Full source

theorem isOpenMap_inr : IsOpenMap (@inr X Y) := fun u hu => by
  simpa [isOpen_sum_iff, preimage_image_eq u Sum.inr_injective]

Right Inclusion is an Open Map for Disjoint Union Topology

Informal description

The right inclusion map $\mathrm{inr} : Y \to X \oplus Y$ is an open map, meaning that for every open set $U \subseteq Y$, the image $\mathrm{inr}(U)$ is open in the disjoint union $X \oplus Y$ equipped with the canonical topology.

isClosedMap_inl theorem

: IsClosedMap (@inl X Y)

Full source

theorem isClosedMap_inl : IsClosedMap (@inl X Y) := fun u hu ↦ by
  simpa [isClosed_sum_iff, preimage_image_eq u Sum.inl_injective]

Left Inclusion is a Closed Map for Disjoint Union Topology

Informal description

The left inclusion map $\mathrm{inl} \colon X \to X \oplus Y$ is a closed map, meaning that for every closed subset $C \subseteq X$, the image $\mathrm{inl}(C)$ is closed in the disjoint union $X \oplus Y$ equipped with the sum topology.

isClosedMap_inr theorem

: IsClosedMap (@inr X Y)

Full source

theorem isClosedMap_inr : IsClosedMap (@inr X Y) := fun u hu ↦ by
  simpa [isClosed_sum_iff, preimage_image_eq u Sum.inr_injective]

Right Inclusion is a Closed Map for Disjoint Union Topology

Informal description

The right inclusion map $\mathrm{inr} : Y \to X \oplus Y$ is a closed map, meaning that for every closed set $C \subseteq Y$, the image $\mathrm{inr}(C)$ is closed in the disjoint union $X \oplus Y$ equipped with the canonical topology.

Topology.IsOpenEmbedding.inl theorem

: IsOpenEmbedding (@inl X Y)

Full source

protected lemma Topology.IsOpenEmbedding.inl : IsOpenEmbedding (@inl X Y) :=
  .of_continuous_injective_isOpenMap continuous_inl inl_injective isOpenMap_inl

Left Inclusion is an Open Embedding for Disjoint Union Topology

Informal description

The left inclusion map $\mathrm{inl} \colon X \to X \oplus Y$ is an open embedding, meaning it is continuous, injective, and maps open sets in $X$ to open sets in the disjoint union $X \oplus Y$ equipped with the sum topology.

Topology.IsOpenEmbedding.inr theorem

: IsOpenEmbedding (@inr X Y)

Full source

protected lemma Topology.IsOpenEmbedding.inr : IsOpenEmbedding (@inr X Y) :=
  .of_continuous_injective_isOpenMap continuous_inr inr_injective isOpenMap_inr

Right Inclusion is an Open Embedding for Disjoint Union Topology

Informal description

The right inclusion map $\mathrm{inr} \colon Y \to X \oplus Y$ is an open embedding, meaning it is injective, continuous, and maps open sets in $Y$ to open sets in the disjoint union $X \oplus Y$ equipped with the canonical topology.

Topology.IsEmbedding.inl theorem

: IsEmbedding (@inl X Y)

Full source

protected lemma Topology.IsEmbedding.inl : IsEmbedding (@inl X Y) := IsOpenEmbedding.inl.1

Left Inclusion is a Topological Embedding for Disjoint Union Topology

Informal description

The left inclusion map $\mathrm{inl} \colon X \to X \oplus Y$ is a topological embedding, meaning it is injective and the topology on $X$ is the coarsest topology that makes $\mathrm{inl}$ continuous. Equivalently, a subset $s \subseteq X$ is open in $X$ if and only if it is the preimage of some open set in $X \oplus Y$ under $\mathrm{inl}$.

Topology.IsEmbedding.inr theorem

: IsEmbedding (@inr X Y)

Full source

protected lemma Topology.IsEmbedding.inr : IsEmbedding (@inr X Y) := IsOpenEmbedding.inr.1

Right Inclusion is a Topological Embedding for Disjoint Union Topology

Informal description

The right inclusion map $\mathrm{inr} \colon Y \to X \oplus Y$ is a topological embedding, meaning it is injective and induces the topology on $Y$ from the disjoint union topology on $X \oplus Y$.

isOpen_range_inl theorem

: IsOpen (range (inl : X → X ⊕ Y))

Full source

lemma isOpen_range_inl : IsOpen (range (inl : X → X ⊕ Y)) := IsOpenEmbedding.inl.2

Openness of Left Inclusion Range in Disjoint Union Topology

Informal description

For any topological spaces $X$ and $Y$, the range of the left inclusion map $\mathrm{inl} \colon X \to X \oplus Y$ is an open subset of the disjoint union $X \oplus Y$ equipped with the sum topology.

isOpen_range_inr theorem

: IsOpen (range (inr : Y → X ⊕ Y))

Full source

lemma isOpen_range_inr : IsOpen (range (inr : Y → X ⊕ Y)) := IsOpenEmbedding.inr.2

Openness of Right Inclusion Range in Disjoint Union Topology

Informal description

For any topological spaces $X$ and $Y$, the range of the right inclusion map $\mathrm{inr} \colon Y \to X \oplus Y$ is an open subset of the disjoint union $X \oplus Y$ equipped with its canonical topology.

isClosed_range_inl theorem

: IsClosed (range (inl : X → X ⊕ Y))

Full source

theorem isClosed_range_inl : IsClosed (range (inl : X → X ⊕ Y)) := by
  rw [← isOpen_compl_iff, compl_range_inl]
  exact isOpen_range_inr

Closedness of Left Inclusion Range in Disjoint Union Topology

Informal description

For any topological spaces $X$ and $Y$, the range of the left inclusion map $\mathrm{inl} \colon X \to X \oplus Y$ is a closed subset of the disjoint union $X \oplus Y$ equipped with the sum topology.

isClosed_range_inr theorem

: IsClosed (range (inr : Y → X ⊕ Y))

Full source

theorem isClosed_range_inr : IsClosed (range (inr : Y → X ⊕ Y)) := by
  rw [← isOpen_compl_iff, compl_range_inr]
  exact isOpen_range_inl

Closedness of Right Inclusion Range in Disjoint Union Topology

Informal description

For any topological spaces $X$ and $Y$, the range of the right inclusion map $\mathrm{inr} \colon Y \to X \oplus Y$ is a closed subset of the disjoint union $X \oplus Y$ equipped with its canonical topology.

Topology.IsClosedEmbedding.inl theorem

: IsClosedEmbedding (inl : X → X ⊕ Y)

Full source

theorem Topology.IsClosedEmbedding.inl : IsClosedEmbedding (inl : X → X ⊕ Y) :=
  ⟨.inl, isClosed_range_inl⟩

Left Inclusion is a Closed Embedding in Disjoint Union Topology

Informal description

The left inclusion map $\mathrm{inl} \colon X \to X \oplus Y$ is a closed embedding, meaning it is injective, continuous, and the image of $X$ under $\mathrm{inl}$ is a closed subset of $X \oplus Y$ with the subspace topology induced by the sum topology.

Topology.IsClosedEmbedding.inr theorem

: IsClosedEmbedding (inr : Y → X ⊕ Y)

Full source

theorem Topology.IsClosedEmbedding.inr : IsClosedEmbedding (inr : Y → X ⊕ Y) :=
  ⟨.inr, isClosed_range_inr⟩

Right Inclusion is a Closed Embedding in Disjoint Union Topology

Informal description

For any topological spaces $X$ and $Y$, the right inclusion map $\mathrm{inr} \colon Y \to X \oplus Y$ is a closed embedding. This means that $\mathrm{inr}$ is injective, continuous, induces the topology on $Y$ from the disjoint union topology on $X \oplus Y$, and has a closed image in $X \oplus Y$.

nhds_inl theorem

(x : X) : 𝓝 (inl x : X ⊕ Y) = map inl (𝓝 x)

Full source

theorem nhds_inl (x : X) : 𝓝 (inl x : X ⊕ Y) = map inl (𝓝 x) :=
  (IsOpenEmbedding.inl.map_nhds_eq _).symm

Neighborhood Filter of Left Inclusion in Disjoint Union

Informal description

For any point $x$ in a topological space $X$, the neighborhood filter of the point $\mathrm{inl}(x)$ in the disjoint union $X \oplus Y$ is equal to the pushforward of the neighborhood filter of $x$ under the left inclusion map $\mathrm{inl} \colon X \to X \oplus Y$. In other words, $\mathcal{N}(\mathrm{inl}(x)) = \mathrm{inl}_*(\mathcal{N}(x))$.

nhds_inr theorem

(y : Y) : 𝓝 (inr y : X ⊕ Y) = map inr (𝓝 y)

Full source

theorem nhds_inr (y : Y) : 𝓝 (inr y : X ⊕ Y) = map inr (𝓝 y) :=
  (IsOpenEmbedding.inr.map_nhds_eq _).symm

Neighborhood Filter of Right Inclusion in Disjoint Union

Informal description

For any point $y$ in a topological space $Y$, the neighborhood filter at $\mathrm{inr}(y)$ in the disjoint union $X \oplus Y$ is equal to the pushforward under $\mathrm{inr}$ of the neighborhood filter at $y$ in $Y$. That is, $\mathcal{N}(\mathrm{inr}(y)) = \mathrm{inr}_*(\mathcal{N}(y))$.

continuous_sumMap theorem

{f : X → Y} {g : Z → W} : Continuous (Sum.map f g) ↔ Continuous f ∧ Continuous g

Full source

@[simp]
theorem continuous_sumMap {f : X → Y} {g : Z → W} :
    ContinuousContinuous (Sum.map f g) ↔ Continuous f ∧ Continuous g :=
  continuous_sumElim.trans <|
    IsEmbedding.inl.continuous_iff.symm.and IsEmbedding.inr.continuous_iff.symm

Continuity of Disjoint Union Map $\text{Sum.map}\, f\, g$ if and only if $f$ and $g$ are Continuous

Informal description

For any topological spaces $X$, $Y$, $Z$, and $W$, the function $\text{Sum.map}\, f\, g \colon X \oplus Z \to Y \oplus W$ is continuous if and only if both $f \colon X \to Y$ and $g \colon Z \to W$ are continuous.

Continuous.sumMap theorem

{f : X → Y} {g : Z → W} (hf : Continuous f) (hg : Continuous g) : Continuous (Sum.map f g)

Full source

@[continuity, fun_prop]
theorem Continuous.sumMap {f : X → Y} {g : Z → W} (hf : Continuous f) (hg : Continuous g) :
    Continuous (Sum.map f g) :=
  continuous_sumMap.2 ⟨hf, hg⟩

Continuity of Disjoint Union Map Induced by Continuous Functions

Informal description

Let $f \colon X \to Y$ and $g \colon Z \to W$ be continuous functions between topological spaces. Then the induced map $\text{Sum.map}\, f\, g \colon X \oplus Z \to Y \oplus W$ on the disjoint unions is also continuous.

isOpenMap_sum theorem

{f : X ⊕ Y → Z} : IsOpenMap f ↔ (IsOpenMap fun a => f (inl a)) ∧ IsOpenMap fun b => f (inr b)

Full source

theorem isOpenMap_sum {f : X ⊕ Y → Z} :
    IsOpenMapIsOpenMap f ↔ (IsOpenMap fun a => f (inl a)) ∧ IsOpenMap fun b => f (inr b) := by
  simp only [isOpenMap_iff_nhds_le, Sum.forall, nhds_inl, nhds_inr, Filter.map_map, comp_def]

Open Map Criterion for Disjoint Union Functions

Informal description

A function $f \colon X \oplus Y \to Z$ between topological spaces is an open map if and only if both the restricted functions $f \circ \mathrm{inl} \colon X \to Z$ and $f \circ \mathrm{inr} \colon Y \to Z$ are open maps.

IsOpenMap.sumMap theorem

{f : X → Y} {g : Z → W} (hf : IsOpenMap f) (hg : IsOpenMap g) : IsOpenMap (Sum.map f g)

Full source

theorem IsOpenMap.sumMap {f : X → Y} {g : Z → W} (hf : IsOpenMap f) (hg : IsOpenMap g) :
    IsOpenMap (Sum.map f g) :=
  isOpenMap_sum.2 ⟨isOpenMap_inl.comp hf, isOpenMap_inr.comp hg⟩

Open Map Property of Sum Maps

Informal description

Let $f \colon X \to Y$ and $g \colon Z \to W$ be open maps between topological spaces. Then the sum map $f \oplus g \colon X \oplus Z \to Y \oplus W$, defined by $(f \oplus g)(\mathrm{inl}\, x) = \mathrm{inl}\, (f x)$ and $(f \oplus g)(\mathrm{inr}\, z) = \mathrm{inr}\, (g z)$, is also an open map.

isOpenMap_sumElim theorem

{f : X → Z} {g : Y → Z} : IsOpenMap (Sum.elim f g) ↔ IsOpenMap f ∧ IsOpenMap g

Full source

@[simp]
theorem isOpenMap_sumElim {f : X → Z} {g : Y → Z} :
    IsOpenMapIsOpenMap (Sum.elim f g) ↔ IsOpenMap f ∧ IsOpenMap g := by
  simp only [isOpenMap_sum, elim_inl, elim_inr]

Open Map Characterization for Disjoint Union Elimination

Informal description

For any functions $f \colon X \to Z$ and $g \colon Y \to Z$ between topological spaces, the function $\mathrm{Sum.elim}\, f\, g \colon X \oplus Y \to Z$ is an open map if and only if both $f$ and $g$ are open maps.

IsOpenMap.sumElim theorem

{f : X → Z} {g : Y → Z} (hf : IsOpenMap f) (hg : IsOpenMap g) : IsOpenMap (Sum.elim f g)

Full source

theorem IsOpenMap.sumElim {f : X → Z} {g : Y → Z} (hf : IsOpenMap f) (hg : IsOpenMap g) :
    IsOpenMap (Sum.elim f g) :=
  isOpenMap_sumElim.2 ⟨hf, hg⟩

Open Map Property of Disjoint Union Elimination

Informal description

For any topological spaces $X$, $Y$, and $Z$, if $f \colon X \to Z$ and $g \colon Y \to Z$ are open maps, then the function $\mathrm{Sum.elim}\, f\, g \colon X \oplus Y \to Z$ is also an open map.

IsOpenEmbedding.sumElim theorem

 {f : X → Z} {g : Y → Z} (hf : IsOpenEmbedding f) (hg : IsOpenEmbedding g) (h : Injective (Sum.elim f g)) :
  IsOpenEmbedding (Sum.elim f g)

Full source

lemma IsOpenEmbedding.sumElim {f : X → Z} {g : Y → Z}
    (hf : IsOpenEmbedding f) (hg : IsOpenEmbedding g) (h : Injective (Sum.elim f g)) :
    IsOpenEmbedding (Sum.elim f g) := by
  rw [isOpenEmbedding_iff_continuous_injective_isOpenMap] at hf hg ⊢
  exact ⟨hf.1.sumElim hg.1, h, hf.2.2.sumElim hg.2.2⟩

Open Embedding Property of Disjoint Union Elimination for Open Embeddings

Informal description

Let $X$, $Y$, and $Z$ be topological spaces, and let $f \colon X \to Z$ and $g \colon Y \to Z$ be open embeddings. If the function $\mathrm{Sum.elim}\, f\, g \colon X \oplus Y \to Z$ is injective, then it is also an open embedding.

isClosedMap_sum theorem

{f : X ⊕ Y → Z} : IsClosedMap f ↔ (IsClosedMap fun a => f (.inl a)) ∧ IsClosedMap fun b => f (.inr b)

Full source

theorem isClosedMap_sum {f : X ⊕ Y → Z} :
    IsClosedMapIsClosedMap f ↔ (IsClosedMap fun a => f (.inl a)) ∧ IsClosedMap fun b => f (.inr b) := by
  constructor
  · intro h
    exact ⟨h.comp IsClosedEmbedding.inl.isClosedMap, h.comp IsClosedEmbedding.inr.isClosedMap⟩
  · rintro h Z hZ
    rw [isClosed_sum_iff] at hZ
    convert (h.1 _ hZ.1).union (h.2 _ hZ.2)
    ext
    simp only [mem_image, Sum.exists, mem_union, mem_preimage]

Closed Map Criterion for Disjoint Union Functions: $f \colon X \oplus Y \to Z$ is closed iff its restrictions to $X$ and $Y$ are closed

Informal description

A function $f \colon X \oplus Y \to Z$ between topological spaces is a closed map if and only if the restrictions $f \circ \mathrm{inl} \colon X \to Z$ and $f \circ \mathrm{inr} \colon Y \to Z$ are both closed maps.

IsClosedMap.sumMap theorem

{f : X → Y} {g : Z → W} (hf : IsClosedMap f) (hg : IsClosedMap g) : IsClosedMap (Sum.map f g)

Full source

theorem IsClosedMap.sumMap {f : X → Y} {g : Z → W} (hf : IsClosedMap f) (hg : IsClosedMap g) :
    IsClosedMap (Sum.map f g) :=
  isClosedMap_sum.2 ⟨isClosedMap_inl.comp hf, isClosedMap_inr.comp hg⟩

Closed Map Property for Disjoint Union of Maps: $f \oplus g$ is closed if $f$ and $g$ are closed

Informal description

Let $f \colon X \to Y$ and $g \colon Z \to W$ be closed maps between topological spaces. Then the induced map $f \oplus g \colon X \oplus Z \to Y \oplus W$ on the disjoint unions is also a closed map.

isClosedMap_sumElim theorem

{f : X → Z} {g : Y → Z} : IsClosedMap (Sum.elim f g) ↔ IsClosedMap f ∧ IsClosedMap g

Full source

@[simp]
theorem isClosedMap_sumElim {f : X → Z} {g : Y → Z} :
    IsClosedMapIsClosedMap (Sum.elim f g) ↔ IsClosedMap f ∧ IsClosedMap g := by
  simp only [isClosedMap_sum, Sum.elim_inl, Sum.elim_inr]

Closed Map Criterion for Disjoint Union Elimination

Informal description

For any functions $f \colon X \to Z$ and $g \colon Y \to Z$ between topological spaces, the function $\mathrm{Sum.elim}\, f\, g \colon X \oplus Y \to Z$ is a closed map if and only if both $f$ and $g$ are closed maps.

IsClosedMap.sumElim theorem

{f : X → Z} {g : Y → Z} (hf : IsClosedMap f) (hg : IsClosedMap g) : IsClosedMap (Sum.elim f g)

Full source

theorem IsClosedMap.sumElim {f : X → Z} {g : Y → Z} (hf : IsClosedMap f) (hg : IsClosedMap g) :
    IsClosedMap (Sum.elim f g) :=
  isClosedMap_sumElim.2 ⟨hf, hg⟩

Closed Map Property for Disjoint Union Elimination

Informal description

For any topological spaces $X$, $Y$, and $Z$, if $f \colon X \to Z$ and $g \colon Y \to Z$ are closed maps, then the function $\mathrm{Sum.elim}\, f\, g \colon X \oplus Y \to Z$ defined by case elimination is also a closed map.

IsClosedEmbedding.sumElim theorem

 {f : X → Z} {g : Y → Z} (hf : IsClosedEmbedding f) (hg : IsClosedEmbedding g) (h : Injective (Sum.elim f g)) :
  IsClosedEmbedding (Sum.elim f g)

Full source

lemma IsClosedEmbedding.sumElim {f : X → Z} {g : Y → Z}
    (hf : IsClosedEmbedding f) (hg : IsClosedEmbedding g) (h : Injective (Sum.elim f g)) :
    IsClosedEmbedding (Sum.elim f g) := by
  rw [IsClosedEmbedding.isClosedEmbedding_iff_continuous_injective_isClosedMap] at hf hg ⊢
  exact ⟨hf.1.sumElim hg.1, h, hf.2.2.sumElim hg.2.2⟩

Closed Embedding Property for Disjoint Union Elimination

Informal description

Let $X$, $Y$, and $Z$ be topological spaces, and let $f \colon X \to Z$ and $g \colon Y \to Z$ be closed embeddings. If the function $\mathrm{Sum.elim}\, f\, g \colon X \oplus Y \to Z$ defined by case elimination is injective, then it is also a closed embedding.

Homeomorph.sumCongr definition

(h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') : X ⊕ Y ≃ₜ X' ⊕ Y'

Full source

/-- Sum of two homeomorphisms. -/
def sumCongr (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') : X ⊕ YX ⊕ Y ≃ₜ X' ⊕ Y' where
  continuous_toFun := h₁.continuous.sumMap h₂.continuous
  continuous_invFun := h₁.symm.continuous.sumMap h₂.symm.continuous
  toEquiv := h₁.toEquiv.sumCongr h₂.toEquiv

Sum of homeomorphisms

Informal description

Given homeomorphisms $h_1 \colon X \simeq_{\text{top}} X'$ and $h_2 \colon Y \simeq_{\text{top}} Y'$ between topological spaces, the sum (disjoint union) homeomorphism $h_1 \oplus h_2 \colon X \oplus Y \simeq_{\text{top}} X' \oplus Y'$ is defined by applying $h_1$ to elements from $X$ and $h_2$ to elements from $Y$, with both the forward and inverse maps being continuous.

Homeomorph.sumCongr_symm theorem

(h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') : (sumCongr h₁ h₂).symm = sumCongr h₁.symm h₂.symm

Full source

@[simp]
lemma sumCongr_symm (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') :
  (sumCongr h₁ h₂).symm = sumCongr h₁.symm h₂.symm := rfl

Inverse of Sum Homeomorphism is Sum of Inverses

Informal description

For any homeomorphisms $h_1 \colon X \simeq_{\text{top}} X'$ and $h_2 \colon Y \simeq_{\text{top}} Y'$ between topological spaces, the inverse of the sum homeomorphism $h_1 \oplus h_2$ is equal to the sum of the inverses $h_1^{-1} \oplus h_2^{-1}$.

Homeomorph.sumCongr_refl theorem

: sumCongr (.refl X) (.refl Y) = .refl (X ⊕ Y)

Full source

@[simp]
theorem sumCongr_refl : sumCongr (.refl X) (.refl Y) = .refl (X ⊕ Y) := by
  ext i
  cases i <;> rfl

Identity Homeomorphism of Disjoint Union: $\text{sumCongr}(\text{refl}_X, \text{refl}_Y) = \text{refl}_{X \oplus Y}$

Informal description

The homeomorphism obtained by taking the disjoint union of the identity homeomorphisms on topological spaces $X$ and $Y$ is equal to the identity homeomorphism on the disjoint union $X \oplus Y$.

Homeomorph.sumCongr_trans theorem

 {X'' Y'' : Type*} [TopologicalSpace X''] [TopologicalSpace Y''] (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') (h₃ : X' ≃ₜ X'')
  (h₄ : Y' ≃ₜ Y'') : (sumCongr h₁ h₂).trans (sumCongr h₃ h₄) = sumCongr (h₁.trans h₃) (h₂.trans h₄)

Full source

@[simp]
theorem sumCongr_trans {X'' Y'' : Type*} [TopologicalSpace X''] [TopologicalSpace Y'']
    (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') (h₃ : X' ≃ₜ X'') (h₄ : Y' ≃ₜ Y'') :
    (sumCongr h₁ h₂).trans (sumCongr h₃ h₄) = sumCongr (h₁.trans h₃) (h₂.trans h₄) := by
  ext i
  cases i <;> rfl

Composition of Sum Homeomorphisms Equals Sum of Compositions

Informal description

Let $X, X', X''$ and $Y, Y', Y''$ be topological spaces. Given homeomorphisms $h_1 \colon X \simeq X'$, $h_2 \colon Y \simeq Y'$, $h_3 \colon X' \simeq X''$, and $h_4 \colon Y' \simeq Y''$, the composition of the sum homeomorphisms $(h_1 \oplus h_2) \circ (h_3 \oplus h_4)$ is equal to the sum homeomorphism of the compositions $(h_1 \circ h_3) \oplus (h_2 \circ h_4)$.

Homeomorph.prodCongr definition

(h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') : X × Y ≃ₜ X' × Y'

Full source

/-- Product of two homeomorphisms. -/
def prodCongr (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') : X × YX × Y ≃ₜ X' × Y' where
  toEquiv := h₁.toEquiv.prodCongr h₂.toEquiv

Homeomorphism of product spaces via component-wise homeomorphisms

Informal description

Given homeomorphisms $ h_1 : X \to X' $ and $ h_2 : Y \to Y' $, the function `Homeomorph.prodCongr` constructs a homeomorphism between the product spaces $ X \times Y $ and $ X' \times Y' $ by applying $ h_1 $ to the first component and $ h_2 $ to the second component of each pair. The inverse is constructed similarly by applying the inverses of $ h_1 $ and $ h_2 $.

Homeomorph.prodCongr_symm theorem

(h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') : (h₁.prodCongr h₂).symm = h₁.symm.prodCongr h₂.symm

Full source

@[simp]
theorem prodCongr_symm (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') :
    (h₁.prodCongr h₂).symm = h₁.symm.prodCongr h₂.symm :=
  rfl

Inverse of Product Homeomorphism Equals Product of Inverses

Informal description

Given homeomorphisms $h_1: X \to X'$ and $h_2: Y \to Y'$, the inverse of the product homeomorphism $h_1 \times h_2: X \times Y \to X' \times Y'$ is equal to the product of the inverses $h_1^{-1} \times h_2^{-1}: X' \times Y' \to X \times Y$.

Homeomorph.coe_prodCongr theorem

(h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') : ⇑(h₁.prodCongr h₂) = Prod.map h₁ h₂

Full source

@[simp]
theorem coe_prodCongr (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') : ⇑(h₁.prodCongr h₂) = Prod.map h₁ h₂ :=
  rfl

Underlying Function of Product Homeomorphism is Product Map

Informal description

Given homeomorphisms $h_1 \colon X \to X'$ and $h_2 \colon Y \to Y'$, the underlying function of the product homeomorphism $h_1 \times h_2 \colon X \times Y \to X' \times Y'$ is equal to the product map $\mathrm{Prod.map}(h_1, h_2)$.

Homeomorph.sumComm definition

: X ⊕ Y ≃ₜ Y ⊕ X

Full source

/-- `X ⊕ Y` is homeomorphic to `Y ⊕ X`. -/
def sumComm : X ⊕ YX ⊕ Y ≃ₜ Y ⊕ X where
  toEquiv := Equiv.sumComm X Y
  continuous_toFun := continuous_sum_swap
  continuous_invFun := continuous_sum_swap

Commutativity of disjoint union of topological spaces

Informal description

The homeomorphism between the disjoint unions $X \oplus Y$ and $Y \oplus X$ of topological spaces, realized by the swap function $\text{Sum.swap} \colon X \oplus Y \to Y \oplus X$ which interchanges the summands. Both the function and its inverse are continuous.

Homeomorph.sumComm_symm theorem

: (sumComm X Y).symm = sumComm Y X

Full source

@[simp]
theorem sumComm_symm : (sumComm X Y).symm = sumComm Y X :=
  rfl

Inverse of Summand-Swapping Homeomorphism Equals Swapped Summand Homeomorphism

Informal description

The inverse of the homeomorphism that swaps the summands of the disjoint union $X \oplus Y$ is equal to the homeomorphism that swaps the summands of $Y \oplus X$. In other words, $(X \oplus Y \simeq_{\text{top}} Y \oplus X)^{-1} = Y \oplus X \simeq_{\text{top}} X \oplus Y$.

Homeomorph.coe_sumComm theorem

: ⇑(sumComm X Y) = Sum.swap

Full source

@[simp]
theorem coe_sumComm : ⇑(sumComm X Y) = Sum.swap :=
  rfl

Underlying Function of Commutativity Homeomorphism for Disjoint Unions

Informal description

The underlying function of the homeomorphism $\text{sumComm}\, X\, Y$ between the disjoint unions $X \oplus Y$ and $Y \oplus X$ is equal to the swap function $\text{Sum.swap} \colon X \oplus Y \to Y \oplus X$.

Homeomorph.continuous_sumAssoc theorem

: Continuous (Equiv.sumAssoc X Y Z)

Full source

@[continuity, fun_prop]
lemma continuous_sumAssoc : Continuous (Equiv.sumAssoc X Y Z) :=
  Continuous.sumElim (by fun_prop) (by fun_prop)

Continuity of the Associativity Bijection for Disjoint Unions of Topological Spaces

Informal description

The canonical associativity bijection $\text{Equiv.sumAssoc} \colon (X \oplus Y) \oplus Z \to X \oplus (Y \oplus Z)$ between the iterated disjoint unions of topological spaces $X$, $Y$, and $Z$ is continuous.

Homeomorph.continuous_sumAssoc_symm theorem

: Continuous (Equiv.sumAssoc X Y Z).symm

Full source

@[continuity, fun_prop]
lemma continuous_sumAssoc_symm : Continuous (Equiv.sumAssoc X Y Z).symm :=
  Continuous.sumElim (by fun_prop) (by fun_prop)

Continuity of the Inverse Associativity Equivalence for Disjoint Unions of Topological Spaces

Informal description

The inverse of the associativity equivalence $(X \oplus Y) \oplus Z \simeq X \oplus (Y \oplus Z)$ is continuous, where $X$, $Y$, and $Z$ are topological spaces and $\oplus$ denotes the disjoint union (sum) of topological spaces.

Homeomorph.sumAssoc definition

: (X ⊕ Y) ⊕ Z ≃ₜ X ⊕ Y ⊕ Z

Full source

/-- `(X ⊕ Y) ⊕ Z` is homeomorphic to `X ⊕ (Y ⊕ Z)`. -/
def sumAssoc : (X ⊕ Y) ⊕ Z(X ⊕ Y) ⊕ Z ≃ₜ X ⊕ Y ⊕ Z where
  toEquiv := Equiv.sumAssoc X Y Z
  continuous_toFun := continuous_sumAssoc X Y Z
  continuous_invFun := continuous_sumAssoc_symm X Y Z

Associativity homeomorphism of disjoint unions

Informal description

The homeomorphism $\text{Homeomorph.sumAssoc}$ provides a continuous bijection between the topological spaces $(X \oplus Y) \oplus Z$ and $X \oplus (Y \oplus Z)$, where $\oplus$ denotes the disjoint union (sum) of topological spaces. The underlying bijection is given by the associativity equivalence of sum types, and both the forward and inverse maps are continuous with respect to the disjoint union topologies.

Homeomorph.sumAssoc_toEquiv theorem

: (sumAssoc X Y Z).toEquiv = Equiv.sumAssoc X Y Z

Full source

@[simp]
lemma sumAssoc_toEquiv : (sumAssoc X Y Z).toEquiv = Equiv.sumAssoc X Y Z := rfl

Underlying Equivalence of Associativity Homeomorphism for Disjoint Unions

Informal description

The underlying equivalence of the associativity homeomorphism between the topological spaces $(X \oplus Y) \oplus Z$ and $X \oplus (Y \oplus Z)$ is equal to the associativity equivalence of sum types, i.e., $\text{sumAssoc}(X, Y, Z).\text{toEquiv} = \text{Equiv.sumAssoc}(X, Y, Z)$.

Homeomorph.sumSumSumComm definition

: (X ⊕ Y) ⊕ W ⊕ Z ≃ₜ (X ⊕ W) ⊕ Y ⊕ Z

Full source

/-- Four-way commutativity of the disjoint union. The name matches `add_add_add_comm`. -/
def sumSumSumComm : (X ⊕ Y) ⊕ W ⊕ Z(X ⊕ Y) ⊕ W ⊕ Z ≃ₜ (X ⊕ W) ⊕ Y ⊕ Z where
  toEquiv := Equiv.sumSumSumComm X Y W Z
  continuous_toFun := by
    unfold Equiv.sumSumSumComm
    dsimp only
    have : Continuous (Sum.map (Sum.map (@id X) ⇑(Equiv.sumComm Y W)) (@id Z)) := by continuity
    fun_prop
  continuous_invFun := by
    unfold Equiv.sumSumSumComm
    dsimp only
    have : Continuous (Sum.map (Sum.map (@id X) (Equiv.sumComm Y W).symm) (@id Z)) := by continuity
    fun_prop

Four-way commutativity homeomorphism of disjoint unions

Informal description

The homeomorphism `Homeomorph.sumSumSumComm` provides a continuous bijection between the topological spaces $(X \oplus Y) \oplus W \oplus Z$ and $(X \oplus W) \oplus Y \oplus Z$, where $\oplus$ denotes the disjoint union (sum) of topological spaces. The underlying bijection is given by the four-way commutativity equivalence of sum types, and both the forward and inverse maps are continuous with respect to the disjoint union topologies.

Homeomorph.sumSumSumComm_toEquiv theorem

: (sumSumSumComm W X Y Z).toEquiv = (Equiv.sumSumSumComm W X Y Z)

Full source

@[simp]
lemma sumSumSumComm_toEquiv : (sumSumSumComm W X Y Z).toEquiv = (Equiv.sumSumSumComm W X Y Z) := rfl

Underlying bijection of four-way commutativity homeomorphism for disjoint unions

Informal description

The underlying bijection of the homeomorphism `sumSumSumComm` between the topological spaces $(W \oplus X) \oplus Y \oplus Z$ and $(W \oplus Y) \oplus X \oplus Z$ is equal to the equivalence `Equiv.sumSumSumComm W X Y Z$.

Homeomorph.sumSumSumComm_symm theorem

: (sumSumSumComm X Y W Z).symm = (sumSumSumComm X W Y Z)

Full source

@[simp]
lemma sumSumSumComm_symm : (sumSumSumComm X Y W Z).symm = (sumSumSumComm X W Y Z) := rfl

Inverse of Four-Way Commutativity Homeomorphism for Disjoint Unions

Informal description

The inverse of the homeomorphism $(X \oplus Y) \oplus W \oplus Z \simeq (X \oplus W) \oplus Y \oplus Z$ is equal to the homeomorphism $(X \oplus W) \oplus Y \oplus Z \simeq (X \oplus Y) \oplus W \oplus Z$.

Homeomorph.prodComm definition

: X × Y ≃ₜ Y × X

Full source

/-- `X × Y` is homeomorphic to `Y × X`. -/
def prodComm : X × YX × Y ≃ₜ Y × X where
  continuous_toFun := continuous_snd.prodMk continuous_fst
  continuous_invFun := continuous_snd.prodMk continuous_fst
  toEquiv := Equiv.prodComm X Y

Commutativity of product spaces via homeomorphism

Informal description

The homeomorphism between the product spaces $X \times Y$ and $Y \times X$ is given by the swap function $(x, y) \mapsto (y, x)$, which is continuous in both directions.

Homeomorph.prodComm_symm theorem

: (prodComm X Y).symm = prodComm Y X

Full source

@[simp]
theorem prodComm_symm : (prodComm X Y).symm = prodComm Y X :=
  rfl

Inverse of Product Commutativity Homeomorphism Equals Swapped Commutativity Homeomorphism

Informal description

The inverse of the homeomorphism swapping the factors of the product space $X \times Y$ is equal to the homeomorphism swapping the factors of $Y \times X$.

Homeomorph.coe_prodComm theorem

: ⇑(prodComm X Y) = Prod.swap

Full source

@[simp]
theorem coe_prodComm : ⇑(prodComm X Y) = Prod.swap :=
  rfl

Homeomorphism between $X \times Y$ and $Y \times X$ is given by swap function

Informal description

The underlying function of the homeomorphism `prodComm X Y` between the product spaces $X \times Y$ and $Y \times X$ is equal to the swap function $\text{Prod.swap} : X \times Y \to Y \times X$ that maps $(x, y)$ to $(y, x)$.

Homeomorph.prodAssoc definition

: (X × Y) × Z ≃ₜ X × Y × Z

Full source

/-- `(X × Y) × Z` is homeomorphic to `X × (Y × Z)`. -/
def prodAssoc : (X × Y) × Z(X × Y) × Z ≃ₜ X × Y × Z where
  continuous_toFun := continuous_fst.fst.prodMk (continuous_fst.snd.prodMk continuous_snd)
  continuous_invFun := (continuous_fst.prodMk continuous_snd.fst).prodMk continuous_snd.snd
  toEquiv := Equiv.prodAssoc X Y Z

Associativity homeomorphism for product spaces

Informal description

The homeomorphism $(X \times Y) \times Z \simeq X \times (Y \times Z)$ reassociates the components of the product space, mapping $((x, y), z)$ to $(x, (y, z))$ and vice versa, while preserving the topological structure.

Homeomorph.prodAssoc_toEquiv theorem

: (prodAssoc X Y Z).toEquiv = Equiv.prodAssoc X Y Z

Full source

@[simp]
lemma prodAssoc_toEquiv : (prodAssoc X Y Z).toEquiv = Equiv.prodAssoc X Y Z := rfl

Equivalence of Associativity Homeomorphism and Type Equivalence for Product Spaces

Informal description

The underlying equivalence of the associativity homeomorphism for product spaces $(X \times Y) \times Z \simeq X \times (Y \times Z)$ is equal to the associativity equivalence for product types $(α × β) × γ ≃ α × (β × γ)$ when applied to the types $X$, $Y$, and $Z$.

Homeomorph.prodProdProdComm definition

: (X × Y) × W × Z ≃ₜ (X × W) × Y × Z

Full source

/-- Four-way commutativity of `prod`. The name matches `mul_mul_mul_comm`. -/
def prodProdProdComm : (X × Y) × W × Z(X × Y) × W × Z ≃ₜ (X × W) × Y × Z where
  toEquiv := Equiv.prodProdProdComm X Y W Z
  continuous_toFun := by
    unfold Equiv.prodProdProdComm
    dsimp only
    fun_prop
  continuous_invFun := by
    unfold Equiv.prodProdProdComm
    dsimp only
    fun_prop

Four-way commutativity homeomorphism for products of topological spaces

Informal description

The homeomorphism between the topological spaces $(X \times Y) \times (W \times Z)$ and $(X \times W) \times (Y \times Z)$ is defined by the bijection that rearranges the components as $((x, y), (w, z)) \mapsto ((x, w), (y, z))$. Both the forward and inverse maps are continuous.

Homeomorph.prodProdProdComm_symm theorem

: (prodProdProdComm X Y W Z).symm = prodProdProdComm X W Y Z

Full source

@[simp]
theorem prodProdProdComm_symm : (prodProdProdComm X Y W Z).symm = prodProdProdComm X W Y Z :=
  rfl

Inverse of Four-Way Product Commutativity Homeomorphism

Informal description

The inverse of the four-way commutativity homeomorphism for products of topological spaces, which maps $(X \times Y) \times (W \times Z)$ to $(X \times W) \times (Y \times Z)$, is equal to the homeomorphism that maps $(X \times W) \times (Y \times Z)$ to $(X \times Y) \times (W \times Z)$.

Homeomorph.prodPUnit definition

: X × PUnit ≃ₜ X

Full source

/-- `X × {*}` is homeomorphic to `X`. -/
@[simps! -fullyApplied apply]
def prodPUnit : X × PUnitX × PUnit ≃ₜ X where
  toEquiv := Equiv.prodPUnit X
  continuous_toFun := continuous_fst
  continuous_invFun := .prodMk_left _

Homeomorphism between $X \times \{\ast\}$ and $X$

Informal description

The product space $X \times \{\ast\}$ is homeomorphic to $X$, where $\{\ast\}$ denotes the unit type with a single element. The homeomorphism is given by the projection onto the first component, which is continuous, and its inverse is the continuous map $x \mapsto (x, \ast)$.

Homeomorph.punitProd definition

: PUnit × X ≃ₜ X

Full source

/-- `{*} × X` is homeomorphic to `X`. -/
def punitProd : PUnitPUnit × XPUnit × X ≃ₜ X :=
  (prodComm _ _).trans (prodPUnit _)

Homeomorphism between $\{\ast\} \times X$ and $X$

Informal description

The product space $\{\ast\} \times X$ is homeomorphic to $X$, where $\{\ast\}$ denotes the unit type with a single element. The homeomorphism is given by the projection onto the second component, which is continuous, and its inverse is the continuous map $x \mapsto (\ast, x)$.

Homeomorph.coe_punitProd theorem

: ⇑(punitProd X) = Prod.snd

Full source

@[simp] theorem coe_punitProd : ⇑(punitProd X) = Prod.snd := rfl

Homeomorphism $\{\ast\} \times X \simeq X$ is given by second projection

Informal description

The underlying function of the homeomorphism $\{\ast\} \times X \simeq X$ is equal to the second projection map $\operatorname{snd} : \{\ast\} \times X \to X$.

Homeomorph.sumEmpty definition

[IsEmpty Y] : X ⊕ Y ≃ₜ X

Full source

/-- The sum of `X` with any empty topological space is homeomorphic to `X`. -/
@[simps! -fullyApplied apply]
def sumEmpty [IsEmpty Y] : X ⊕ YX ⊕ Y ≃ₜ X where
  toEquiv := Equiv.sumEmpty X Y
  continuous_toFun := Continuous.sumElim continuous_id (by fun_prop)
  continuous_invFun := continuous_inl

Homeomorphism between a space and its disjoint union with an empty space

Informal description

Given a topological space $X$ and an empty topological space $Y$ (i.e., `IsEmpty Y` holds), the disjoint union $X \oplus Y$ is homeomorphic to $X$. The homeomorphism is given by the equivalence that maps $\text{inl}(x)$ to $x$ for any $x \in X$ and is undefined on $\text{inr}(y)$ (since $Y$ is empty). The homeomorphism is continuous in both directions.

Homeomorph.emptySum definition

[IsEmpty Y] : Y ⊕ X ≃ₜ X

Full source

/-- The sum of `X` with any empty topological space is homeomorphic to `X`. -/
def emptySum [IsEmpty Y] : Y ⊕ XY ⊕ X ≃ₜ X := (sumComm Y X).trans (sumEmpty X Y)

Homeomorphism between a space and the disjoint union with an empty space (left version)

Informal description

Given a topological space $X$ and an empty topological space $Y$ (i.e., $Y$ has no elements), the disjoint union $Y \oplus X$ is homeomorphic to $X$. This homeomorphism is constructed by first swapping the summands via the canonical homeomorphism $Y \oplus X \simeq X \oplus Y$, and then applying the homeomorphism $X \oplus Y \simeq X$ (which exists because $Y$ is empty).

Homeomorph.coe_emptySum theorem

[IsEmpty Y] : (emptySum X Y).toEquiv = Equiv.emptySum Y X

Full source

@[simp] theorem coe_emptySum [IsEmpty Y] : (emptySum X Y).toEquiv = Equiv.emptySum Y X := rfl

Underlying Equivalence of Empty Sum Homeomorphism

Informal description

For any topological space $X$ and an empty topological space $Y$ (i.e., $Y$ has no elements), the underlying equivalence of the homeomorphism `emptySum X Y` is equal to the equivalence `Equiv.emptySum Y X` that maps the sum type $Y \oplus X$ to $X$.

Homeomorph.sumProdDistrib definition

: (X ⊕ Y) × Z ≃ₜ (X × Z) ⊕ (Y × Z)

Full source

/-- `(X ⊕ Y) × Z` is homeomorphic to `X × Z ⊕ Y × Z`. -/
@[simps!]
def sumProdDistrib : (X ⊕ Y) × Z(X ⊕ Y) × Z ≃ₜ (X × Z) ⊕ (Y × Z) :=
  Homeomorph.symm <|
    (Equiv.sumProdDistrib X Y Z).symm.toHomeomorphOfContinuousOpen
        ((continuous_inl.prodMap continuous_id).sumElim
          (continuous_inr.prodMap continuous_id)) <|
      (isOpenMap_inl.prodMap IsOpenMap.id).sumElim (isOpenMap_inr.prodMap IsOpenMap.id)

Right distributive homeomorphism for products over sums

Informal description

The product space $(X \oplus Y) \times Z$ is homeomorphic to the disjoint union of product spaces $(X \times Z) \oplus (Y \times Z)$. This homeomorphism demonstrates the right distributivity of products over disjoint unions in the category of topological spaces.

Homeomorph.prodSumDistrib definition

: X × (Y ⊕ Z) ≃ₜ (X × Y) ⊕ (X × Z)

Full source

/-- `X × (Y ⊕ Z)` is homeomorphic to `X × Y ⊕ X × Z`. -/
def prodSumDistrib : X × (Y ⊕ Z)X × (Y ⊕ Z) ≃ₜ (X × Y) ⊕ (X × Z) :=
  (prodComm _ _).trans <| sumProdDistrib.trans <| sumCongr (prodComm _ _) (prodComm _ _)

Left distributive homeomorphism for products over sums

Informal description

The product space $X \times (Y \oplus Z)$ is homeomorphic to the disjoint union of product spaces $(X \times Y) \oplus (X \times Z)$. This homeomorphism demonstrates the left distributivity of products over disjoint unions in the category of topological spaces.

Mathlib.Topology.Constructions.SumProd

Implementation note

Tags