Mathlib.Topology.ContinuousOn

nhds_bind_nhdsWithin theorem

{a : α} {s : Set α} : ((𝓝 a).bind fun x => 𝓝[s] x) = 𝓝[s] a

Full source

@[simp]
theorem nhds_bind_nhdsWithin {a : α} {s : Set α} : ((𝓝 a).bind fun x => 𝓝[s] x) = 𝓝[s] a :=
  bind_inf_principal.trans <| congr_arg₂ _ nhds_bind_nhds rfl

Neighborhood Filter Binding Equals Neighborhood Filter Within Subset

Informal description

For any point $a$ in a topological space $\alpha$ and any subset $s \subseteq \alpha$, the filter obtained by binding the neighborhood filter $\mathfrak{N}(a)$ with the function $x \mapsto \mathfrak{N}[s]x$ (the neighborhood filter of $x$ within $s$) is equal to the neighborhood filter of $a$ within $s$, i.e., \[ \mathfrak{N}(a) \bind (\lambda x, \mathfrak{N}[s]x) = \mathfrak{N}[s]a. \]

eventually_nhds_nhdsWithin theorem

 {a : α} {s : Set α} {p : α → Prop} : (∀ᶠ y in 𝓝 a, ∀ᶠ x in 𝓝[s] y, p x) ↔ ∀ᶠ x in 𝓝[s] a, p x

Full source

@[simp]
theorem eventually_nhds_nhdsWithin {a : α} {s : Set α} {p : α → Prop} :
    (∀ᶠ y in 𝓝 a, ∀ᶠ x in 𝓝[s] y, p x) ↔ ∀ᶠ x in 𝓝[s] a, p x :=
  Filter.ext_iff.1 nhds_bind_nhdsWithin { x | p x }

Equivalence of Nested Neighborhood Filters Within a Subset

Informal description

For any point $a$ in a topological space $\alpha$, any subset $s \subseteq \alpha$, and any predicate $p$ on $\alpha$, the following are equivalent: 1. For every point $y$ in a neighborhood of $a$, the predicate $p$ holds for all $x$ in the neighborhood of $y$ within $s$. 2. The predicate $p$ holds for all $x$ in the neighborhood of $a$ within $s$. In other words, the following equivalence holds: \[ (\forall y \text{ near } a, \forall x \text{ near } y \text{ within } s, p(x)) \leftrightarrow (\forall x \text{ near } a \text{ within } s, p(x)). \]

eventually_nhdsWithin_iff theorem

{a : α} {s : Set α} {p : α → Prop} : (∀ᶠ x in 𝓝[s] a, p x) ↔ ∀ᶠ x in 𝓝 a, x ∈ s → p x

Full source

theorem eventually_nhdsWithin_iff {a : α} {s : Set α} {p : α → Prop} :
    (∀ᶠ x in 𝓝[s] a, p x) ↔ ∀ᶠ x in 𝓝 a, x ∈ s → p x :=
  eventually_inf_principal

Equivalence of Neighborhood Filter Within and Implication in Full Neighborhood

Informal description

For any point $a$ in a topological space $\alpha$, any subset $s \subseteq \alpha$, and any predicate $p$ on $\alpha$, the following are equivalent: 1. The predicate $p$ holds for all points $x$ in the neighborhood of $a$ within $s$ (i.e., $\forallᶠ x \in \mathfrak{N}[s]a, p(x)$). 2. The implication $x \in s \rightarrow p(x)$ holds for all points $x$ in the neighborhood of $a$ (i.e., $\forallᶠ x \in \mathfrak{N}a, x \in s \rightarrow p(x)$).

frequently_nhdsWithin_iff theorem

{z : α} {s : Set α} {p : α → Prop} : (∃ᶠ x in 𝓝[s] z, p x) ↔ ∃ᶠ x in 𝓝 z, p x ∧ x ∈ s

Full source

theorem frequently_nhdsWithin_iff {z : α} {s : Set α} {p : α → Prop} :
    (∃ᶠ x in 𝓝[s] z, p x) ↔ ∃ᶠ x in 𝓝 z, p x ∧ x ∈ s :=
  frequently_inf_principal.trans <| by simp only [and_comm]

Frequently Within Neighborhoods Equivalence

Informal description

For a point $z$ in a topological space $\alpha$, a set $s \subseteq \alpha$, and a predicate $p : \alpha \to \text{Prop}$, the following are equivalent: 1. There exists a frequently occurring $x$ in the neighborhood of $z$ within $s$ such that $p(x)$ holds. 2. There exists a frequently occurring $x$ in the neighborhood of $z$ such that $p(x)$ holds and $x \in s$. Here, "frequently occurring" means that the set of such $x$ is not eventually negligible in the respective filter.

mem_closure_ne_iff_frequently_within theorem

{z : α} {s : Set α} : z ∈ closure (s \ { z }) ↔ ∃ᶠ x in 𝓝[≠] z, x ∈ s

Full source

theorem mem_closure_ne_iff_frequently_within {z : α} {s : Set α} :
    z ∈ closure (s \ {z})z ∈ closure (s \ {z}) ↔ ∃ᶠ x in 𝓝[≠] z, x ∈ s := by
  simp [mem_closure_iff_frequently, frequently_nhdsWithin_iff]

Characterization of Limit Points via Neighborhood Filter

Informal description

For any point $z$ in a topological space $\alpha$ and any subset $s \subseteq \alpha$, the point $z$ belongs to the closure of $s \setminus \{z\}$ if and only if there exists a neighborhood filter $\mathcal{N}_{z}^{\neq}$ (the filter of neighborhoods of $z$ excluding $z$ itself) such that $x \in s$ holds frequently in this filter. In other words, $z \in \overline{s \setminus \{z\}}$ if and only if there are points $x$ arbitrarily close to $z$ (but not equal to $z$) that belong to $s$.

eventually_eventually_nhdsWithin theorem

 {a : α} {s : Set α} {p : α → Prop} : (∀ᶠ y in 𝓝[s] a, ∀ᶠ x in 𝓝[s] y, p x) ↔ ∀ᶠ x in 𝓝[s] a, p x

Full source

@[simp]
theorem eventually_eventually_nhdsWithin {a : α} {s : Set α} {p : α → Prop} :
    (∀ᶠ y in 𝓝[s] a, ∀ᶠ x in 𝓝[s] y, p x) ↔ ∀ᶠ x in 𝓝[s] a, p x := by
  refine ⟨fun h => ?_, fun h => (eventually_nhds_nhdsWithin.2 h).filter_mono inf_le_left⟩
  simp only [eventually_nhdsWithin_iff] at h ⊢
  exact h.mono fun x hx hxs => (hx hxs).self_of_nhds hxs

Equivalence of Nested Neighborhood Filters Within a Subset

Informal description

For any point $a$ in a topological space $\alpha$, any subset $s \subseteq \alpha$, and any predicate $p$ on $\alpha$, the following are equivalent: 1. For every point $y$ in the neighborhood of $a$ within $s$, the predicate $p$ holds for all $x$ in the neighborhood of $y$ within $s$. 2. The predicate $p$ holds for all $x$ in the neighborhood of $a$ within $s$. In other words, the following equivalence holds: \[ (\forall y \text{ near } a \text{ within } s, \forall x \text{ near } y \text{ within } s, p(x)) \leftrightarrow (\forall x \text{ near } a \text{ within } s, p(x)). \]

eventually_mem_nhdsWithin_iff theorem

{x : α} {s t : Set α} : (∀ᶠ x' in 𝓝[s] x, t ∈ 𝓝[s] x') ↔ t ∈ 𝓝[s] x

Full source

@[simp]
theorem eventually_mem_nhdsWithin_iff {x : α} {s t : Set α} :
    (∀ᶠ x' in 𝓝[s] x, t ∈ 𝓝[s] x') ↔ t ∈ 𝓝[s] x :=
  eventually_eventually_nhdsWithin

Equivalence of Neighborhood Membership in Restricted Neighborhood Filters

Informal description

For any point $x$ in a topological space $\alpha$ and any subsets $s, t \subseteq \alpha$, the following are equivalent: 1. For all points $x'$ in the neighborhood of $x$ within $s$, the set $t$ is in the neighborhood filter of $x'$ within $s$. 2. The set $t$ is in the neighborhood filter of $x$ within $s$. In other words: \[ (\forall x' \text{ near } x \text{ within } s, t \text{ is a neighborhood of } x' \text{ within } s) \leftrightarrow t \text{ is a neighborhood of } x \text{ within } s. \]

nhdsWithin_eq theorem

(a : α) (s : Set α) : 𝓝[s] a = ⨅ t ∈ {t : Set α | a ∈ t ∧ IsOpen t}, 𝓟 (t ∩ s)

Full source

theorem nhdsWithin_eq (a : α) (s : Set α) :
    𝓝[s] a = ⨅ t ∈ { t : Set α | a ∈ t ∧ IsOpen t }, 𝓟 (t ∩ s) :=
  ((nhds_basis_opens a).inf_principal s).eq_biInf

Characterization of Neighborhood Filter within a Subset

Informal description

For any point $a$ in a topological space $\alpha$ and any subset $s \subseteq \alpha$, the neighborhood filter $\mathcal{N}_s(a)$ of $a$ within $s$ is equal to the infimum of the principal filters of the intersections $t \cap s$ over all open sets $t$ containing $a$. In symbols: \[ \mathcal{N}_s(a) = \biginf_{t \text{ open}, a \in t} \mathcal{P}(t \cap s) \] where $\mathcal{P}(t \cap s)$ denotes the principal filter generated by the set $t \cap s$.

nhdsWithin_univ theorem

(a : α) : 𝓝[Set.univ] a = 𝓝 a

Full source

@[simp] lemma nhdsWithin_univ (a : α) : 𝓝[Set.univ] a = 𝓝 a := by
  rw [nhdsWithin, principal_univ, inf_top_eq]

Neighborhood Filter within Entire Space Equals Ordinary Neighborhood Filter

Informal description

For any point $a$ in a topological space $\alpha$, the neighborhood filter of $a$ within the entire space (i.e., $\mathcal{N}_{\text{univ}}(a)$) is equal to the ordinary neighborhood filter $\mathcal{N}(a)$ of $a$.

nhdsWithin_hasBasis theorem

 {ι : Sort*} {p : ι → Prop} {s : ι → Set α} {a : α} (h : (𝓝 a).HasBasis p s) (t : Set α) :
  (𝓝[t] a).HasBasis p fun i => s i ∩ t

Full source

theorem nhdsWithin_hasBasis {ι : Sort*} {p : ι → Prop} {s : ι → Set α} {a : α}
    (h : (𝓝 a).HasBasis p s) (t : Set α) : (𝓝[t] a).HasBasis p fun i => s i ∩ t :=
  h.inf_principal t

Basis for Relative Neighborhood Filter via Intersection

Informal description

Let $\alpha$ be a topological space, $a \in \alpha$, and $t \subseteq \alpha$. Suppose the neighborhood filter $\mathcal{N}(a)$ has a basis $\{s_i\}_{i \in \iota}$ indexed by a predicate $p$ (i.e., for any $i$ satisfying $p$, $s_i$ is a neighborhood of $a$). Then the relative neighborhood filter $\mathcal{N}_t(a)$ (neighborhoods of $a$ within $t$) has basis $\{s_i \cap t\}_{i \in \iota}$ indexed by the same predicate $p$.

nhdsWithin_basis_open theorem

(a : α) (t : Set α) : (𝓝[t] a).HasBasis (fun u => a ∈ u ∧ IsOpen u) fun u => u ∩ t

Full source

theorem nhdsWithin_basis_open (a : α) (t : Set α) :
    (𝓝[t] a).HasBasis (fun u => a ∈ ua ∈ u ∧ IsOpen u) fun u => u ∩ t :=
  nhdsWithin_hasBasis (nhds_basis_opens a) t

Basis for Relative Neighborhood Filter via Open Sets

Informal description

Let $\alpha$ be a topological space, $a \in \alpha$, and $t \subseteq \alpha$. The neighborhood filter $\mathcal{N}_t(a)$ (neighborhoods of $a$ within $t$) has a basis consisting of sets of the form $u \cap t$, where $u$ is an open set containing $a$.

mem_nhdsWithin theorem

{t : Set α} {a : α} {s : Set α} : t ∈ 𝓝[s] a ↔ ∃ u, IsOpen u ∧ a ∈ u ∧ u ∩ s ⊆ t

Full source

theorem mem_nhdsWithin {t : Set α} {a : α} {s : Set α} :
    t ∈ 𝓝[s] at ∈ 𝓝[s] a ↔ ∃ u, IsOpen u ∧ a ∈ u ∧ u ∩ s ⊆ t := by
  simpa only [and_assoc, and_left_comm] using (nhdsWithin_basis_open a s).mem_iff

Characterization of Relative Neighborhoods via Open Sets

Informal description

For a topological space $\alpha$, a point $a \in \alpha$, and subsets $s, t \subseteq \alpha$, the set $t$ is a neighborhood of $a$ within $s$ (denoted $t \in \mathcal{N}_s(a)$) if and only if there exists an open set $u$ containing $a$ such that $u \cap s \subseteq t$.

mem_nhdsWithin_iff_exists_mem_nhds_inter theorem

{t : Set α} {a : α} {s : Set α} : t ∈ 𝓝[s] a ↔ ∃ u ∈ 𝓝 a, u ∩ s ⊆ t

Full source

theorem mem_nhdsWithin_iff_exists_mem_nhds_inter {t : Set α} {a : α} {s : Set α} :
    t ∈ 𝓝[s] at ∈ 𝓝[s] a ↔ ∃ u ∈ 𝓝 a, u ∩ s ⊆ t :=
  (nhdsWithin_hasBasis (𝓝 a).basis_sets s).mem_iff

Characterization of Relative Neighborhoods via Intersection

Informal description

A subset $t$ of a topological space $\alpha$ is a neighborhood of a point $a$ within a subset $s$ (i.e., $t \in \mathcal{N}_s(a)$) if and only if there exists a neighborhood $u$ of $a$ in $\alpha$ (i.e., $u \in \mathcal{N}(a)$) such that the intersection $u \cap s$ is contained in $t$.

diff_mem_nhdsWithin_compl theorem

{x : α} {s : Set α} (hs : s ∈ 𝓝 x) (t : Set α) : s \ t ∈ 𝓝[tᶜ] x

Full source

theorem diff_mem_nhdsWithin_compl {x : α} {s : Set α} (hs : s ∈ 𝓝 x) (t : Set α) :
    s \ ts \ t ∈ 𝓝[tᶜ] x :=
  diff_mem_inf_principal_compl hs t

Neighborhood difference property in complement subspace

Informal description

Let $X$ be a topological space, $x \in X$, and $s \subseteq X$ be a neighborhood of $x$ (i.e., $s \in \mathcal{N}(x)$). Then for any subset $t \subseteq X$, the set difference $s \setminus t$ is a neighborhood of $x$ within the complement $t^c$, i.e., $s \setminus t \in \mathcal{N}_{t^c}(x)$.

diff_mem_nhdsWithin_diff theorem

{x : α} {s t : Set α} (hs : s ∈ 𝓝[t] x) (t' : Set α) : s \ t' ∈ 𝓝[t \ t'] x

Full source

theorem diff_mem_nhdsWithin_diff {x : α} {s t : Set α} (hs : s ∈ 𝓝[t] x) (t' : Set α) :
    s \ t's \ t' ∈ 𝓝[t \ t'] x := by
  rw [nhdsWithin, diff_eq, diff_eq, ← inf_principal, ← inf_assoc]
  exact inter_mem_inf hs (mem_principal_self _)

Neighborhood difference property in relative difference subspace

Informal description

Let $X$ be a topological space, $x \in X$, and $s, t \subseteq X$ such that $s$ is a neighborhood of $x$ within $t$ (i.e., $s \in \mathcal{N}_t(x)$). Then for any subset $t' \subseteq X$, the set difference $s \setminus t'$ is a neighborhood of $x$ within $t \setminus t'$ (i.e., $s \setminus t' \in \mathcal{N}_{t \setminus t'}(x)$).

nhds_of_nhdsWithin_of_nhds theorem

{s t : Set α} {a : α} (h1 : s ∈ 𝓝 a) (h2 : t ∈ 𝓝[s] a) : t ∈ 𝓝 a

Full source

theorem nhds_of_nhdsWithin_of_nhds {s t : Set α} {a : α} (h1 : s ∈ 𝓝 a) (h2 : t ∈ 𝓝[s] a) :
    t ∈ 𝓝 a := by
  rcases mem_nhdsWithin_iff_exists_mem_nhds_inter.mp h2 with ⟨_, Hw, hw⟩
  exact (𝓝 a).sets_of_superset ((𝓝 a).inter_sets Hw h1) hw

Neighborhood Inheritance from Relative Neighborhood

Informal description

Let $X$ be a topological space, $a \in X$, and $s, t \subseteq X$. If $s$ is a neighborhood of $a$ (i.e., $s \in \mathcal{N}(a)$) and $t$ is a neighborhood of $a$ within $s$ (i.e., $t \in \mathcal{N}_s(a)$), then $t$ is a neighborhood of $a$ in $X$ (i.e., $t \in \mathcal{N}(a)$).

mem_nhdsWithin_iff_eventually theorem

{s t : Set α} {x : α} : t ∈ 𝓝[s] x ↔ ∀ᶠ y in 𝓝 x, y ∈ s → y ∈ t

Full source

theorem mem_nhdsWithin_iff_eventually {s t : Set α} {x : α} :
    t ∈ 𝓝[s] xt ∈ 𝓝[s] x ↔ ∀ᶠ y in 𝓝 x, y ∈ s → y ∈ t :=
  eventually_inf_principal

Characterization of Neighborhoods Within a Set via Eventual Membership

Informal description

For any sets $s, t$ in a topological space and a point $x$, the set $t$ is a neighborhood of $x$ within $s$ (denoted $t \in \mathcal{N}_s(x)$) if and only if, for all $y$ sufficiently close to $x$, whenever $y \in s$ then $y \in t$.

mem_nhdsWithin_iff_eventuallyEq theorem

{s t : Set α} {x : α} : t ∈ 𝓝[s] x ↔ s =ᶠ[𝓝 x] (s ∩ t : Set α)

Full source

theorem mem_nhdsWithin_iff_eventuallyEq {s t : Set α} {x : α} :
    t ∈ 𝓝[s] xt ∈ 𝓝[s] x ↔ s =ᶠ[𝓝 x] (s ∩ t : Set α) := by
  simp_rw [mem_nhdsWithin_iff_eventually, eventuallyEq_set, mem_inter_iff, iff_self_and]

Characterization of Neighborhoods Within a Set via Eventual Equality

Informal description

For any sets $s, t$ in a topological space $\alpha$ and any point $x \in \alpha$, the set $t$ is in the neighborhood filter of $x$ within $s$ if and only if $s$ is eventually equal to $s \cap t$ in the neighborhood filter of $x$. In other words, $t \in \mathcal{N}_s(x) \leftrightarrow s =_{\mathcal{N}(x)} (s \cap t)$.

nhdsWithin_eq_iff_eventuallyEq theorem

{s t : Set α} {x : α} : 𝓝[s] x = 𝓝[t] x ↔ s =ᶠ[𝓝 x] t

Full source

theorem nhdsWithin_eq_iff_eventuallyEq {s t : Set α} {x : α} : 𝓝[s] x𝓝[s] x = 𝓝[t] x ↔ s =ᶠ[𝓝 x] t :=
  set_eventuallyEq_iff_inf_principal.symm

Equality of Neighborhood Filters Within Sets is Equivalent to Eventual Equality of Sets

Informal description

For any sets $s, t$ in a topological space $\alpha$ and any point $x \in \alpha$, the neighborhood filters $\mathcal{N}_s(x)$ and $\mathcal{N}_t(x)$ within $s$ and $t$ respectively are equal if and only if $s$ and $t$ are eventually equal in the neighborhood filter of $x$. That is, $\mathcal{N}_s(x) = \mathcal{N}_t(x) \leftrightarrow s =_{\mathcal{N}(x)} t$.

nhdsWithin_le_iff theorem

{s t : Set α} {x : α} : 𝓝[s] x ≤ 𝓝[t] x ↔ t ∈ 𝓝[s] x

Full source

theorem nhdsWithin_le_iff {s t : Set α} {x : α} : 𝓝[s] x𝓝[s] x ≤ 𝓝[t] x ↔ t ∈ 𝓝[s] x :=
  set_eventuallyLE_iff_inf_principal_le.symm.trans set_eventuallyLE_iff_mem_inf_principal

Neighborhood Filter Comparison Criterion: $\mathcal{N}_s(x) \leq \mathcal{N}_t(x) \leftrightarrow t \in \mathcal{N}_s(x)$

Informal description

For any sets $s, t$ in a topological space $\alpha$ and any point $x \in \alpha$, the neighborhood filter of $x$ within $s$ is finer than the neighborhood filter of $x$ within $t$ if and only if $t$ is a neighborhood of $x$ within $s$.

preimage_nhdsWithin_coinduced' theorem

 {π : α → β} {s : Set β} {t : Set α} {a : α} (h : a ∈ t)
  (hs : s ∈ @nhds β (.coinduced (fun x : t => π x) inferInstance) (π a)) : π ⁻¹' s ∈ 𝓝[t] a

Full source

theorem preimage_nhdsWithin_coinduced' {π : α → β} {s : Set β} {t : Set α} {a : α} (h : a ∈ t)
    (hs : s ∈ @nhds β (.coinduced (fun x : t => π x) inferInstance) (π a)) :
    π ⁻¹' sπ ⁻¹' s ∈ 𝓝[t] a := by
  lift a to t using h
  replace hs : (fun x : t => π x) ⁻¹' s(fun x : t => π x) ⁻¹' s ∈ 𝓝 a := preimage_nhds_coinduced hs
  rwa [← map_nhds_subtype_val, mem_map]

Preimage of Neighborhood in Coinduced Topology is Neighborhood in Subspace

Informal description

Let $\pi : \alpha \to \beta$ be a function between topological spaces, $s \subseteq \beta$ a subset, $t \subseteq \alpha$ a subset, and $a \in t$ a point. If $s$ is a neighborhood of $\pi(a)$ in the topology on $\beta$ coinduced by the restriction of $\pi$ to $t$, then the preimage $\pi^{-1}(s)$ is a neighborhood of $a$ in the subspace topology of $t$.

mem_nhdsWithin_of_mem_nhds theorem

{s t : Set α} {a : α} (h : s ∈ 𝓝 a) : s ∈ 𝓝[t] a

Full source

theorem mem_nhdsWithin_of_mem_nhds {s t : Set α} {a : α} (h : s ∈ 𝓝 a) : s ∈ 𝓝[t] a :=
  mem_inf_of_left h

Neighborhood Inclusion in Subset Context

Informal description

For any sets $s, t$ in a topological space $\alpha$ and any point $a \in \alpha$, if $s$ is a neighborhood of $a$, then $s$ is also a neighborhood of $a$ within $t$.

self_mem_nhdsWithin theorem

{a : α} {s : Set α} : s ∈ 𝓝[s] a

Full source

theorem self_mem_nhdsWithin {a : α} {s : Set α} : s ∈ 𝓝[s] a :=
  mem_inf_of_right (mem_principal_self s)

Self-Neighborhood Property in Subset Topology

Informal description

For any point $a$ in a topological space $\alpha$ and any subset $s \subseteq \alpha$, the set $s$ is a neighborhood of $a$ within $s$ itself. In other words, $s \in \mathcal{N}_s(a)$, where $\mathcal{N}_s(a)$ denotes the neighborhood filter of $a$ relative to $s$.

eventually_mem_nhdsWithin theorem

{a : α} {s : Set α} : ∀ᶠ x in 𝓝[s] a, x ∈ s

Full source

theorem eventually_mem_nhdsWithin {a : α} {s : Set α} : ∀ᶠ x in 𝓝[s] a, x ∈ s :=
  self_mem_nhdsWithin

Eventual Membership in Relative Neighborhoods

Informal description

For any point $a$ in a topological space $\alpha$ and any subset $s \subseteq \alpha$, eventually every point $x$ in the neighborhood filter of $a$ relative to $s$ belongs to $s$. In other words, $\forall x \in \mathcal{N}_s(a)$, eventually $x \in s$.

inter_mem_nhdsWithin theorem

(s : Set α) {t : Set α} {a : α} (h : t ∈ 𝓝 a) : s ∩ t ∈ 𝓝[s] a

Full source

theorem inter_mem_nhdsWithin (s : Set α) {t : Set α} {a : α} (h : t ∈ 𝓝 a) : s ∩ ts ∩ t ∈ 𝓝[s] a :=
  inter_mem self_mem_nhdsWithin (mem_inf_of_left h)

Intersection with Neighborhood Preserves Relative Neighborhood

Informal description

For any subset $s$ of a topological space $\alpha$, any neighborhood $t$ of a point $a \in \alpha$ (i.e., $t \in \mathcal{N}(a)$), the intersection $s \cap t$ is a neighborhood of $a$ within $s$ (i.e., $s \cap t \in \mathcal{N}_s(a)$).

pure_le_nhdsWithin theorem

{a : α} {s : Set α} (ha : a ∈ s) : pure a ≤ 𝓝[s] a

Full source

theorem pure_le_nhdsWithin {a : α} {s : Set α} (ha : a ∈ s) : pure a ≤ 𝓝[s] a :=
  le_inf (pure_le_nhds a) (le_principal_iff.2 ha)

Pure Filter is Contained in Relative Neighborhood Filter

Informal description

For any point $a$ in a topological space $\alpha$ and any subset $s \subseteq \alpha$ containing $a$, the pure filter at $a$ is contained in the neighborhood filter of $a$ relative to $s$. In other words, if $a \in s$, then $\{a\} \subseteq \mathcal{N}_s(a)$.

mem_of_mem_nhdsWithin theorem

{a : α} {s t : Set α} (ha : a ∈ s) (ht : t ∈ 𝓝[s] a) : a ∈ t

Full source

theorem mem_of_mem_nhdsWithin {a : α} {s t : Set α} (ha : a ∈ s) (ht : t ∈ 𝓝[s] a) : a ∈ t :=
  pure_le_nhdsWithin ha ht

Membership in Relative Neighborhood Implies Membership in Set

Informal description

For any point $a$ in a topological space $\alpha$ and any subsets $s, t \subseteq \alpha$, if $a \in s$ and $t$ is a neighborhood of $a$ within $s$ (i.e., $t \in \mathcal{N}_s(a)$), then $a \in t$.

Filter.Eventually.self_of_nhdsWithin theorem

{p : α → Prop} {s : Set α} {x : α} (h : ∀ᶠ y in 𝓝[s] x, p y) (hx : x ∈ s) : p x

Full source

theorem Filter.Eventually.self_of_nhdsWithin {p : α → Prop} {s : Set α} {x : α}
    (h : ∀ᶠ y in 𝓝[s] x, p y) (hx : x ∈ s) : p x :=
  mem_of_mem_nhdsWithin hx h

Pointwise Property from Relative Neighborhood Property

Informal description

For any predicate $p$ on a topological space $\alpha$, any subset $s \subseteq \alpha$, and any point $x \in s$, if $p(y)$ holds for all $y$ in some neighborhood of $x$ within $s$ (i.e., $\forall y \in \mathcal{N}_s(x), p(y)$), then $p(x)$ holds.

tendsto_const_nhdsWithin theorem

{l : Filter β} {s : Set α} {a : α} (ha : a ∈ s) : Tendsto (fun _ : β => a) l (𝓝[s] a)

Full source

theorem tendsto_const_nhdsWithin {l : Filter β} {s : Set α} {a : α} (ha : a ∈ s) :
    Tendsto (fun _ : β => a) l (𝓝[s] a) :=
  tendsto_const_pure.mono_right <| pure_le_nhdsWithin ha

Limit of Constant Function in Subspace Topology

Informal description

For any filter $l$ on a type $\beta$, any subset $s$ of a topological space $\alpha$, and any point $a \in s$, the constant function mapping every element of $\beta$ to $a$ tends to $a$ within $s$ with respect to the filter $l$. In other words, the function $\lambda \_ \colon \beta \to a$ satisfies $\lim_{l} (\lambda \_ \colon \beta \to a) = a$ in the subspace topology of $s$.

nhdsWithin_restrict'' theorem

{a : α} (s : Set α) {t : Set α} (h : t ∈ 𝓝[s] a) : 𝓝[s] a = 𝓝[s ∩ t] a

Full source

theorem nhdsWithin_restrict'' {a : α} (s : Set α) {t : Set α} (h : t ∈ 𝓝[s] a) :
    𝓝[s] a = 𝓝[s ∩ t] a :=
  le_antisymm (le_inf inf_le_left (le_principal_iff.mpr (inter_mem self_mem_nhdsWithin h)))
    (inf_le_inf_left _ (principal_mono.mpr Set.inter_subset_left))

Restriction of Neighborhood Filter to Smaller Neighborhood

Informal description

For any point $a$ in a topological space $\alpha$, any subset $s \subseteq \alpha$, and any subset $t \subseteq \alpha$ such that $t$ is a neighborhood of $a$ within $s$ (i.e., $t \in \mathcal{N}_s(a)$), the neighborhood filter of $a$ within $s$ is equal to the neighborhood filter of $a$ within $s \cap t$.

nhdsWithin_restrict' theorem

{a : α} (s : Set α) {t : Set α} (h : t ∈ 𝓝 a) : 𝓝[s] a = 𝓝[s ∩ t] a

Full source

theorem nhdsWithin_restrict' {a : α} (s : Set α) {t : Set α} (h : t ∈ 𝓝 a) : 𝓝[s] a = 𝓝[s ∩ t] a :=
  nhdsWithin_restrict'' s <| mem_inf_of_left h

Restriction of Relative Neighborhood Filter to Smaller Neighborhood

Informal description

For any point $a$ in a topological space $\alpha$, any subset $s \subseteq \alpha$, and any subset $t \subseteq \alpha$ such that $t$ is a neighborhood of $a$ (i.e., $t \in \mathcal{N}(a)$), the neighborhood filter of $a$ within $s$ is equal to the neighborhood filter of $a$ within $s \cap t$.

nhdsWithin_restrict theorem

{a : α} (s : Set α) {t : Set α} (h₀ : a ∈ t) (h₁ : IsOpen t) : 𝓝[s] a = 𝓝[s ∩ t] a

Full source

theorem nhdsWithin_restrict {a : α} (s : Set α) {t : Set α} (h₀ : a ∈ t) (h₁ : IsOpen t) :
    𝓝[s] a = 𝓝[s ∩ t] a :=
  nhdsWithin_restrict' s (IsOpen.mem_nhds h₁ h₀)

Restriction of Relative Neighborhood Filter to Open Neighborhood

Informal description

For any point $a$ in a topological space $\alpha$, any subset $s \subseteq \alpha$, and any open subset $t \subseteq \alpha$ containing $a$, the neighborhood filter of $a$ within $s$ is equal to the neighborhood filter of $a$ within $s \cap t$.

nhdsWithin_le_of_mem theorem

{a : α} {s t : Set α} (h : s ∈ 𝓝[t] a) : 𝓝[t] a ≤ 𝓝[s] a

Full source

theorem nhdsWithin_le_of_mem {a : α} {s t : Set α} (h : s ∈ 𝓝[t] a) : 𝓝[t] a ≤ 𝓝[s] a :=
  nhdsWithin_le_iff.mpr h

Neighborhood Filter Refinement: $\mathcal{N}_t(a) \leq \mathcal{N}_s(a)$ when $s \in \mathcal{N}_t(a)$

Informal description

For any point $a$ in a topological space $\alpha$ and any sets $s, t \subseteq \alpha$, if $s$ is a neighborhood of $a$ within $t$, then the neighborhood filter of $a$ within $t$ is finer than the neighborhood filter of $a$ within $s$, i.e., $\mathcal{N}_t(a) \leq \mathcal{N}_s(a)$.

nhdsWithin_le_nhds theorem

{a : α} {s : Set α} : 𝓝[s] a ≤ 𝓝 a

Full source

theorem nhdsWithin_le_nhds {a : α} {s : Set α} : 𝓝[s] a ≤ 𝓝 a := by
  rw [← nhdsWithin_univ]
  apply nhdsWithin_le_of_mem
  exact univ_mem

Neighborhood Filter within Subset is Finer than Ordinary Neighborhood Filter

Informal description

For any point $a$ in a topological space $\alpha$ and any subset $s \subseteq \alpha$, the neighborhood filter of $a$ within $s$ is finer than the ordinary neighborhood filter of $a$, i.e., $\mathcal{N}_s(a) \leq \mathcal{N}(a)$.

nhdsWithin_eq_nhdsWithin' theorem

{a : α} {s t u : Set α} (hs : s ∈ 𝓝 a) (h₂ : t ∩ s = u ∩ s) : 𝓝[t] a = 𝓝[u] a

Full source

theorem nhdsWithin_eq_nhdsWithin' {a : α} {s t u : Set α} (hs : s ∈ 𝓝 a) (h₂ : t ∩ s = u ∩ s) :
    𝓝[t] a = 𝓝[u] a := by rw [nhdsWithin_restrict' t hs, nhdsWithin_restrict' u hs, h₂]

Equality of Relative Neighborhood Filters via Common Intersection

Informal description

For any point $a$ in a topological space $\alpha$ and any subsets $s, t, u \subseteq \alpha$, if $s$ is a neighborhood of $a$ (i.e., $s \in \mathcal{N}(a)$) and the intersections $t \cap s$ and $u \cap s$ are equal, then the neighborhood filters of $a$ within $t$ and $u$ are equal, i.e., $\mathcal{N}_t(a) = \mathcal{N}_u(a)$.

nhdsWithin_eq_nhdsWithin theorem

{a : α} {s t u : Set α} (h₀ : a ∈ s) (h₁ : IsOpen s) (h₂ : t ∩ s = u ∩ s) : 𝓝[t] a = 𝓝[u] a

Full source

theorem nhdsWithin_eq_nhdsWithin {a : α} {s t u : Set α} (h₀ : a ∈ s) (h₁ : IsOpen s)
    (h₂ : t ∩ s = u ∩ s) : 𝓝[t] a = 𝓝[u] a := by
  rw [nhdsWithin_restrict t h₀ h₁, nhdsWithin_restrict u h₀ h₁, h₂]

Equality of Relative Neighborhood Filters via Open Intersection

Informal description

For any point $a$ in a topological space $\alpha$ and any subsets $s, t, u \subseteq \alpha$, if $s$ is an open set containing $a$ and the intersections $t \cap s$ and $u \cap s$ are equal, then the neighborhood filters of $a$ within $t$ and $u$ are equal, i.e., $\mathcal{N}_t(a) = \mathcal{N}_u(a)$.

nhdsWithin_eq_nhds theorem

{a : α} {s : Set α} : 𝓝[s] a = 𝓝 a ↔ s ∈ 𝓝 a

Full source

@[simp] theorem nhdsWithin_eq_nhds {a : α} {s : Set α} : 𝓝[s] a𝓝[s] a = 𝓝 a ↔ s ∈ 𝓝 a :=
  inf_eq_left.trans le_principal_iff

Equality of Relative and Full Neighborhood Filters at a Point

Informal description

For a point $a$ in a topological space and a subset $s$, the neighborhood filter of $a$ within $s$ is equal to the full neighborhood filter of $a$ if and only if $s$ is a neighborhood of $a$. In other words, $\mathcal{N}_s(a) = \mathcal{N}(a) \leftrightarrow s \in \mathcal{N}(a)$.

IsOpen.nhdsWithin_eq theorem

{a : α} {s : Set α} (h : IsOpen s) (ha : a ∈ s) : 𝓝[s] a = 𝓝 a

Full source

theorem IsOpen.nhdsWithin_eq {a : α} {s : Set α} (h : IsOpen s) (ha : a ∈ s) : 𝓝[s] a = 𝓝 a :=
  nhdsWithin_eq_nhds.2 <| h.mem_nhds ha

Equality of Relative and Full Neighborhood Filters for Open Sets

Informal description

For any open set $s$ in a topological space and any point $a \in s$, the neighborhood filter of $a$ within $s$ equals the full neighborhood filter of $a$, i.e., $\mathcal{N}_s(a) = \mathcal{N}(a)$.

preimage_nhds_within_coinduced theorem

 {π : α → β} {s : Set β} {t : Set α} {a : α} (h : a ∈ t) (ht : IsOpen t)
  (hs : s ∈ @nhds β (.coinduced (fun x : t => π x) inferInstance) (π a)) : π ⁻¹' s ∈ 𝓝 a

Full source

theorem preimage_nhds_within_coinduced {π : α → β} {s : Set β} {t : Set α} {a : α} (h : a ∈ t)
    (ht : IsOpen t)
    (hs : s ∈ @nhds β (.coinduced (fun x : t => π x) inferInstance) (π a)) :
    π ⁻¹' sπ ⁻¹' s ∈ 𝓝 a := by
  rw [← ht.nhdsWithin_eq h]
  exact preimage_nhdsWithin_coinduced' h hs

Preimage of Coinduced Neighborhood in Open Subset is Neighborhood

Informal description

Let $\pi : \alpha \to \beta$ be a function between topological spaces, $s \subseteq \beta$ a subset, $t \subseteq \alpha$ an open subset, and $a \in t$ a point. If $s$ is a neighborhood of $\pi(a)$ in the topology on $\beta$ coinduced by the restriction of $\pi$ to $t$, then the preimage $\pi^{-1}(s)$ is a neighborhood of $a$ in $\alpha$.

nhdsWithin_empty theorem

(a : α) : 𝓝[∅] a = ⊥

Full source

@[simp]
theorem nhdsWithin_empty (a : α) : 𝓝[∅] a = ⊥ := by rw [nhdsWithin, principal_empty, inf_bot_eq]

Neighborhood Filter within Empty Set is Bottom

Informal description

For any point $a$ in a topological space $\alpha$, the neighborhood filter of $a$ within the empty set is equal to the bottom element of the filter lattice, i.e., $\mathcal{N}_\emptyset(a) = \bot$.

nhdsWithin_union theorem

(a : α) (s t : Set α) : 𝓝[s ∪ t] a = 𝓝[s] a ⊔ 𝓝[t] a

Full source

theorem nhdsWithin_union (a : α) (s t : Set α) : 𝓝[s ∪ t] a = 𝓝[s] a𝓝[s] a ⊔ 𝓝[t] a := by
  delta nhdsWithin
  rw [← inf_sup_left, sup_principal]

Neighborhood Filter of Union Equals Supremum of Neighborhood Filters

Informal description

For any point $a$ in a topological space $\alpha$ and any sets $s, t \subseteq \alpha$, the neighborhood filter of $a$ within the union $s \cup t$ is equal to the supremum of the neighborhood filters of $a$ within $s$ and within $t$, i.e., \[ \mathcal{N}_{s \cup t}(a) = \mathcal{N}_s(a) \sqcup \mathcal{N}_t(a). \]

nhds_eq_nhdsWithin_sup_nhdsWithin theorem

(b : α) {I₁ I₂ : Set α} (hI : Set.univ = I₁ ∪ I₂) : nhds b = nhdsWithin b I₁ ⊔ nhdsWithin b I₂

Full source

theorem nhds_eq_nhdsWithin_sup_nhdsWithin (b : α) {I₁ I₂ : Set α} (hI : Set.univ = I₁ ∪ I₂) :
    nhds b = nhdsWithinnhdsWithin b I₁ ⊔ nhdsWithin b I₂ := by
  rw [← nhdsWithin_univ b, hI, nhdsWithin_union]

Neighborhood Filter Decomposition via Relative Neighborhoods

Informal description

For any point $b$ in a topological space $\alpha$ and any sets $I_1, I_2 \subseteq \alpha$ such that $I_1 \cup I_2 = \alpha$, the neighborhood filter of $b$ is equal to the supremum of the neighborhood filters of $b$ within $I_1$ and within $I_2$, i.e., \[ \mathcal{N}(b) = \mathcal{N}_{I_1}(b) \sqcup \mathcal{N}_{I_2}(b). \]

union_mem_nhds_of_mem_nhdsWithin theorem

 {b : α} {I₁ I₂ : Set α} (h : Set.univ = I₁ ∪ I₂) {L : Set α} (hL : L ∈ nhdsWithin b I₁) {R : Set α}
  (hR : R ∈ nhdsWithin b I₂) : L ∪ R ∈ nhds b

Full source

/-- If `L` and `R` are neighborhoods of `b` within sets whose union is `Set.univ`, then
`L ∪ R` is a neighborhood of `b`. -/
theorem union_mem_nhds_of_mem_nhdsWithin {b : α}
    {I₁ I₂ : Set α} (h : Set.univ = I₁ ∪ I₂)
    {L : Set α} (hL : L ∈ nhdsWithin b I₁)
    {R : Set α} (hR : R ∈ nhdsWithin b I₂) : L ∪ RL ∪ R ∈ nhds b := by
  rw [← nhdsWithin_univ b, h, nhdsWithin_union]
  exact ⟨mem_of_superset hL (by simp), mem_of_superset hR (by simp)⟩

Union of Relative Neighborhoods is a Neighborhood

Informal description

Let $\alpha$ be a topological space, and let $b \in \alpha$. Suppose $I_1$ and $I_2$ are subsets of $\alpha$ such that $I_1 \cup I_2 = \alpha$. If $L$ is a neighborhood of $b$ within $I_1$ and $R$ is a neighborhood of $b$ within $I_2$, then $L \cup R$ is a neighborhood of $b$.

punctured_nhds_eq_nhdsWithin_sup_nhdsWithin theorem

[LinearOrder α] {x : α} : 𝓝[≠] x = 𝓝[<] x ⊔ 𝓝[>] x

Full source

/-- Writing a punctured neighborhood filter as a sup of left and right filters. -/
lemma punctured_nhds_eq_nhdsWithin_sup_nhdsWithin [LinearOrder α] {x : α} :
    𝓝[≠] x = 𝓝[<] x𝓝[<] x ⊔ 𝓝[>] x := by
  rw [← Iio_union_Ioi, nhdsWithin_union]

Punctured Neighborhood Filter Decomposition in Linear Order

Informal description

For any element $x$ in a linearly ordered topological space $\alpha$, the punctured neighborhood filter of $x$ (i.e., the filter of neighborhoods of $x$ excluding $x$ itself) is equal to the supremum of the neighborhood filters of $x$ restricted to the sets $(-\infty, x)$ and $(x, \infty)$. In other words, \[ \mathcal{N}_{\neq x}(x) = \mathcal{N}_{x}(x). \]

nhds_of_Ici_Iic theorem

 [LinearOrder α] {b : α} {L : Set α} (hL : L ∈ 𝓝[≤] b) {R : Set α} (hR : R ∈ 𝓝[≥] b) : L ∩ Iic b ∪ R ∩ Ici b ∈ 𝓝 b

Full source

/-- Obtain a "predictably-sided" neighborhood of `b` from two one-sided neighborhoods. -/
theorem nhds_of_Ici_Iic [LinearOrder α] {b : α}
    {L : Set α} (hL : L ∈ 𝓝[≤] b)
    {R : Set α} (hR : R ∈ 𝓝[≥] b) : L ∩ Iic bL ∩ Iic b ∪ R ∩ Ici bL ∩ Iic b ∪ R ∩ Ici b ∈ 𝓝 b :=
  union_mem_nhds_of_mem_nhdsWithin Iic_union_Ici.symm
    (inter_mem hL self_mem_nhdsWithin) (inter_mem hR self_mem_nhdsWithin)

Neighborhood Construction from Left and Right Relative Neighborhoods in Linear Order

Informal description

Let $\alpha$ be a linearly ordered topological space and $b \in \alpha$. If $L$ is a neighborhood of $b$ within the closed left-infinite interval $(-\infty, b]$ and $R$ is a neighborhood of $b$ within the closed right-infinite interval $[b, \infty)$, then the union of $L \cap (-\infty, b]$ and $R \cap [b, \infty)$ is a neighborhood of $b$.

nhdsWithin_biUnion theorem

{ι} {I : Set ι} (hI : I.Finite) (s : ι → Set α) (a : α) : 𝓝[⋃ i ∈ I, s i] a = ⨆ i ∈ I, 𝓝[s i] a

Full source

theorem nhdsWithin_biUnion {ι} {I : Set ι} (hI : I.Finite) (s : ι → Set α) (a : α) :
    𝓝[⋃ i ∈ I, s i] a = ⨆ i ∈ I, 𝓝[s i] a := by
  induction I, hI using Set.Finite.induction_on with
  | empty => simp
  | insert _ _ hT => simp only [hT, nhdsWithin_union, iSup_insert, biUnion_insert]

Neighborhood Filter within Finite Union Equals Supremum of Neighborhood Filters

Informal description

Let $\alpha$ be a topological space, $\iota$ an index type, $I \subseteq \iota$ a finite subset, and $s : \iota \to \text{Set } \alpha$ a family of subsets of $\alpha$. For any point $a \in \alpha$, the neighborhood filter of $a$ within the union $\bigcup_{i \in I} s(i)$ is equal to the supremum of the neighborhood filters of $a$ within each $s(i)$ for $i \in I$. In symbols: \[ \mathcal{N}_{\bigcup_{i \in I} s(i)}(a) = \bigsqcup_{i \in I} \mathcal{N}_{s(i)}(a). \]

nhdsWithin_sUnion theorem

{S : Set (Set α)} (hS : S.Finite) (a : α) : 𝓝[⋃₀ S] a = ⨆ s ∈ S, 𝓝[s] a

Full source

theorem nhdsWithin_sUnion {S : Set (Set α)} (hS : S.Finite) (a : α) :
    𝓝[⋃₀ S] a = ⨆ s ∈ S, 𝓝[s] a := by
  rw [sUnion_eq_biUnion, nhdsWithin_biUnion hS]

Neighborhood Filter within Finite Union of Sets Equals Supremum of Neighborhood Filters

Informal description

Let $\alpha$ be a topological space, $S$ a finite collection of subsets of $\alpha$, and $a \in \alpha$. The neighborhood filter of $a$ within the union $\bigcup_{s \in S} s$ is equal to the supremum of the neighborhood filters of $a$ within each $s \in S$. In symbols: \[ \mathcal{N}_{\bigcup S}(a) = \bigsqcup_{s \in S} \mathcal{N}_s(a). \]

nhdsWithin_iUnion theorem

{ι} [Finite ι] (s : ι → Set α) (a : α) : 𝓝[⋃ i, s i] a = ⨆ i, 𝓝[s i] a

Full source

theorem nhdsWithin_iUnion {ι} [Finite ι] (s : ι → Set α) (a : α) :
    𝓝[⋃ i, s i] a = ⨆ i, 𝓝[s i] a := by
  rw [← sUnion_range, nhdsWithin_sUnion (finite_range s), iSup_range]

Neighborhood Filter within Finite Union Equals Supremum of Neighborhood Filters

Informal description

Let $\alpha$ be a topological space, $\iota$ a finite index type, and $s : \iota \to \text{Set } \alpha$ a family of subsets of $\alpha$. For any point $a \in \alpha$, the neighborhood filter of $a$ within the union $\bigcup_{i \in \iota} s(i)$ is equal to the supremum of the neighborhood filters of $a$ within each $s(i)$. In symbols: \[ \mathcal{N}_{\bigcup_{i} s(i)}(a) = \bigsqcup_{i} \mathcal{N}_{s(i)}(a). \]

nhdsWithin_inter theorem

(a : α) (s t : Set α) : 𝓝[s ∩ t] a = 𝓝[s] a ⊓ 𝓝[t] a

Full source

theorem nhdsWithin_inter (a : α) (s t : Set α) : 𝓝[s ∩ t] a = 𝓝[s] a𝓝[s] a ⊓ 𝓝[t] a := by
  delta nhdsWithin
  rw [inf_left_comm, inf_assoc, inf_principal, ← inf_assoc, inf_idem]

Neighborhood Filter of Intersection Equals Infimum of Neighborhood Filters

Informal description

For any point $a$ in a topological space $\alpha$ and any subsets $s, t \subseteq \alpha$, the neighborhood filter of $a$ within the intersection $s \cap t$ is equal to the infimum of the neighborhood filters of $a$ within $s$ and within $t$. That is, \[ \mathcal{N}_{s \cap t}(a) = \mathcal{N}_s(a) \sqcap \mathcal{N}_t(a) \] where $\mathcal{N}_s(a)$ denotes the neighborhood filter of $a$ within $s$.

nhdsWithin_inter' theorem

(a : α) (s t : Set α) : 𝓝[s ∩ t] a = 𝓝[s] a ⊓ 𝓟 t

Full source

theorem nhdsWithin_inter' (a : α) (s t : Set α) : 𝓝[s ∩ t] a = 𝓝[s] a𝓝[s] a ⊓ 𝓟 t := by
  delta nhdsWithin
  rw [← inf_principal, inf_assoc]

Neighborhood Filter of Intersection Equals Infimum with Principal Filter

Informal description

For any point $a$ in a topological space $\alpha$ and any subsets $s, t \subseteq \alpha$, the neighborhood filter of $a$ within $s \cap t$ is equal to the infimum of the neighborhood filter of $a$ within $s$ and the principal filter of $t$.

nhdsWithin_inter_of_mem theorem

{a : α} {s t : Set α} (h : s ∈ 𝓝[t] a) : 𝓝[s ∩ t] a = 𝓝[t] a

Full source

theorem nhdsWithin_inter_of_mem {a : α} {s t : Set α} (h : s ∈ 𝓝[t] a) : 𝓝[s ∩ t] a = 𝓝[t] a := by
  rw [nhdsWithin_inter, inf_eq_right]
  exact nhdsWithin_le_of_mem h

Neighborhood Filter Equality for Intersection with Neighborhood Set

Informal description

For any point $a$ in a topological space $\alpha$ and any subsets $s, t \subseteq \alpha$, if $s$ is a neighborhood of $a$ within $t$ (i.e., $s \in \mathcal{N}_t(a)$), then the neighborhood filter of $a$ within $s \cap t$ is equal to the neighborhood filter of $a$ within $t$, i.e., $\mathcal{N}_{s \cap t}(a) = \mathcal{N}_t(a)$.

nhdsWithin_inter_of_mem' theorem

{a : α} {s t : Set α} (h : t ∈ 𝓝[s] a) : 𝓝[s ∩ t] a = 𝓝[s] a

Full source

theorem nhdsWithin_inter_of_mem' {a : α} {s t : Set α} (h : t ∈ 𝓝[s] a) : 𝓝[s ∩ t] a = 𝓝[s] a := by
  rw [inter_comm, nhdsWithin_inter_of_mem h]

Neighborhood Filter Equality for Intersection with Neighborhood Set (Symmetric Version)

Informal description

For any point $a$ in a topological space $\alpha$ and any subsets $s, t \subseteq \alpha$, if $t$ is a neighborhood of $a$ within $s$ (i.e., $t \in \mathcal{N}_s(a)$), then the neighborhood filter of $a$ within $s \cap t$ is equal to the neighborhood filter of $a$ within $s$, i.e., $\mathcal{N}_{s \cap t}(a) = \mathcal{N}_s(a)$.

nhdsWithin_singleton theorem

(a : α) : 𝓝[{ a }] a = pure a

Full source

@[simp]
theorem nhdsWithin_singleton (a : α) : 𝓝[{a}] a = pure a := by
  rw [nhdsWithin, principal_singleton, inf_eq_right.2 (pure_le_nhds a)]

Neighborhood Filter at a Singleton Set Equals Pure Filter

Informal description

For any point $a$ in a topological space $\alpha$, the neighborhood filter of $a$ within the singleton set $\{a\}$ is equal to the pure filter at $a$, i.e., $\mathcal{N}_{\{a\}}(a) = \text{pure}(a)$.

nhdsWithin_insert theorem

(a : α) (s : Set α) : 𝓝[insert a s] a = pure a ⊔ 𝓝[s] a

Full source

@[simp]
theorem nhdsWithin_insert (a : α) (s : Set α) : 𝓝[insert a s] a = purepure a ⊔ 𝓝[s] a := by
  rw [← singleton_union, nhdsWithin_union, nhdsWithin_singleton]

Neighborhood Filter of Inserted Point Equals Supremum of Pure and Neighborhood Filters

Informal description

For any point $a$ in a topological space $\alpha$ and any subset $s \subseteq \alpha$, the neighborhood filter of $a$ within the set $\{a\} \cup s$ is equal to the supremum of the pure filter at $a$ and the neighborhood filter of $a$ within $s$, i.e., \[ \mathcal{N}_{\{a\} \cup s}(a) = \text{pure}(a) \sqcup \mathcal{N}_s(a). \]

mem_nhdsWithin_insert theorem

{a : α} {s t : Set α} : t ∈ 𝓝[insert a s] a ↔ a ∈ t ∧ t ∈ 𝓝[s] a

Full source

theorem mem_nhdsWithin_insert {a : α} {s t : Set α} : t ∈ 𝓝[insert a s] at ∈ 𝓝[insert a s] a ↔ a ∈ t ∧ t ∈ 𝓝[s] a := by
  simp

Characterization of Neighborhoods in an Inserted Set

Informal description

For any point $a$ in a topological space $\alpha$, any subset $s \subseteq \alpha$, and any set $t \subseteq \alpha$, the set $t$ belongs to the neighborhood filter of $a$ within $\{a\} \cup s$ if and only if $a \in t$ and $t$ belongs to the neighborhood filter of $a$ within $s$. In symbols: \[ t \in \mathcal{N}_{\{a\} \cup s}(a) \leftrightarrow (a \in t) \land (t \in \mathcal{N}_s(a)). \]

insert_mem_nhdsWithin_insert theorem

{a : α} {s t : Set α} (h : t ∈ 𝓝[s] a) : insert a t ∈ 𝓝[insert a s] a

Full source

theorem insert_mem_nhdsWithin_insert {a : α} {s t : Set α} (h : t ∈ 𝓝[s] a) :
    insertinsert a t ∈ 𝓝[insert a s] a := by simp [mem_of_superset h]

Insertion Preserves Neighborhood Membership in Augmented Set

Informal description

For any point $a$ in a topological space $\alpha$ and any subsets $s, t \subseteq \alpha$, if $t$ belongs to the neighborhood filter of $a$ within $s$, then the set $\{a\} \cup t$ belongs to the neighborhood filter of $a$ within $\{a\} \cup s$.

insert_mem_nhds_iff theorem

{a : α} {s : Set α} : insert a s ∈ 𝓝 a ↔ s ∈ 𝓝[≠] a

Full source

theorem insert_mem_nhds_iff {a : α} {s : Set α} : insertinsert a s ∈ 𝓝 ainsert a s ∈ 𝓝 a ↔ s ∈ 𝓝[≠] a := by
  simp only [nhdsWithin, mem_inf_principal, mem_compl_iff, mem_singleton_iff, or_iff_not_imp_left,
    insert_def]

Neighborhood characterization via insertion at a point

Informal description

For a point $a$ in a topological space and a set $s$, the set $\{a\} \cup s$ is a neighborhood of $a$ if and only if $s$ is a neighborhood of $a$ in the subspace topology of the complement of $\{a\}$.

nhdsNE_sup_pure theorem

(a : α) : 𝓝[≠] a ⊔ pure a = 𝓝 a

Full source

@[simp]
theorem nhdsNE_sup_pure (a : α) : 𝓝[≠] a𝓝[≠] a ⊔ pure a = 𝓝 a := by
  rw [← nhdsWithin_singleton, ← nhdsWithin_union, compl_union_self, nhdsWithin_univ]

Decomposition of Neighborhood Filter into Neighborhood Filter at Complement and Pure Filter

Informal description

For any point $a$ in a topological space $\alpha$, the supremum of the neighborhood filter of $a$ within the complement of $\{a\}$ and the pure filter at $a$ is equal to the neighborhood filter of $a$, i.e., \[ \mathcal{N}_{\neq a}(a) \sqcup \text{pure}(a) = \mathcal{N}(a). \]

pure_sup_nhdsNE theorem

(a : α) : pure a ⊔ 𝓝[≠] a = 𝓝 a

Full source

@[simp]
theorem pure_sup_nhdsNE (a : α) : purepure a ⊔ 𝓝[≠] a = 𝓝 a := by rw [← sup_comm, nhdsNE_sup_pure]

Neighborhood Filter Decomposition via Pure and Complement Filters

Informal description

For any point $a$ in a topological space $\alpha$, the supremum of the pure filter at $a$ and the neighborhood filter of $a$ within the complement of $\{a\}$ is equal to the neighborhood filter of $a$, i.e., \[ \text{pure}(a) \sqcup \mathcal{N}_{\neq a}(a) = \mathcal{N}(a). \]

nhdsWithin_prod theorem

 [TopologicalSpace β] {s u : Set α} {t v : Set β} {a : α} {b : β} (hu : u ∈ 𝓝[s] a) (hv : v ∈ 𝓝[t] b) :
  u ×ˢ v ∈ 𝓝[s ×ˢ t] (a, b)

Full source

theorem nhdsWithin_prod [TopologicalSpace β]
    {s u : Set α} {t v : Set β} {a : α} {b : β} (hu : u ∈ 𝓝[s] a) (hv : v ∈ 𝓝[t] b) :
    u ×ˢ v ∈ 𝓝[s ×ˢ t] (a, b) := by
  rw [nhdsWithin_prod_eq]
  exact prod_mem_prod hu hv

Product of Neighborhoods Within Sets is Neighborhood Within Product Set

Informal description

Let $α$ and $β$ be topological spaces, with $s \subseteq α$, $t \subseteq β$, $a \in α$, and $b \in β$. If $u$ is a neighborhood of $a$ within $s$ (i.e., $u \in \mathcal{N}_s(a)$) and $v$ is a neighborhood of $b$ within $t$ (i.e., $v \in \mathcal{N}_t(b)$), then the product set $u \times v$ is a neighborhood of $(a,b)$ within $s \times t$ (i.e., $u \times v \in \mathcal{N}_{s \times t}((a,b))$).

Filter.EventuallyEq.mem_interior theorem

{x : α} {s t : Set α} (hst : s =ᶠ[𝓝 x] t) (h : x ∈ interior s) : x ∈ interior t

Full source

lemma Filter.EventuallyEq.mem_interior {x : α} {s t : Set α} (hst : s =ᶠ[𝓝 x] t)
    (h : x ∈ interior s) : x ∈ interior t := by
  rw [← nhdsWithin_eq_iff_eventuallyEq] at hst
  simpa [mem_interior_iff_mem_nhds, ← nhdsWithin_eq_nhds, hst] using h

Eventual Equality Preserves Interior Membership

Informal description

For any point $x$ in a topological space $\alpha$ and any sets $s, t \subseteq \alpha$, if $s$ and $t$ are eventually equal in the neighborhood filter of $x$ (i.e., $s =_{\mathcal{N}(x)} t$) and $x$ belongs to the interior of $s$, then $x$ also belongs to the interior of $t$.

Filter.EventuallyEq.mem_interior_iff theorem

{x : α} {s t : Set α} (hst : s =ᶠ[𝓝 x] t) : x ∈ interior s ↔ x ∈ interior t

Full source

lemma Filter.EventuallyEq.mem_interior_iff {x : α} {s t : Set α} (hst : s =ᶠ[𝓝 x] t) :
    x ∈ interior sx ∈ interior s ↔ x ∈ interior t :=
  ⟨fun h ↦ hst.mem_interior h, fun h ↦ hst.symm.mem_interior h⟩

Interior Membership Criterion via Eventual Equality in Neighborhoods

Informal description

For any point $x$ in a topological space $\alpha$ and any sets $s, t \subseteq \alpha$, if $s$ and $t$ are eventually equal in the neighborhood filter of $x$ (i.e., $s =_{\mathcal{N}(x)} t$), then $x$ belongs to the interior of $s$ if and only if $x$ belongs to the interior of $t$.

nhdsWithin_pi_eq' theorem

 {I : Set ι} (hI : I.Finite) (s : ∀ i, Set (π i)) (x : ∀ i, π i) :
  𝓝[pi I s] x = ⨅ i, comap (fun x => x i) (𝓝 (x i) ⊓ ⨅ (_ : i ∈ I), 𝓟 (s i))

Full source

theorem nhdsWithin_pi_eq' {I : Set ι} (hI : I.Finite) (s : ∀ i, Set (π i)) (x : ∀ i, π i) :
    𝓝[pi I s] x = ⨅ i, comap (fun x => x i) (𝓝 (x i) ⊓ ⨅ (_ : i ∈ I), 𝓟 (s i)) := by
  simp only [nhdsWithin, nhds_pi, Filter.pi, comap_inf, comap_iInf, pi_def, comap_principal, ←
    iInf_principal_finite hI, ← iInf_inf_eq]

Neighborhood Filter within Finite Product Set as Infimum of Projected Filters

Informal description

For a finite index set $I \subseteq \iota$ and for each $i \in \iota$, a set $s_i \subseteq \pi_i$ and a point $x = (x_i)_{i \in \iota}$ in the product space $\prod_{i \in \iota} \pi_i$, the neighborhood filter within the product set $\prod_{i \in I} s_i$ at $x$ is equal to the infimum over all $i \in \iota$ of the pullback under the projection $\pi_i$ of the intersection of the neighborhood filter at $x_i$ with the principal filter of $s_i$ for $i \in I$. In symbols: \[ \mathcal{N}_{\prod_{i \in I} s_i}(x) = \bigsqcap_{i \in \iota} \text{comap}_{\pi_i} \left( \mathcal{N}(x_i) \sqcap \bigsqcap_{i \in I} \mathcal{P}(s_i) \right) \]

nhdsWithin_pi_eq theorem

 {I : Set ι} (hI : I.Finite) (s : ∀ i, Set (π i)) (x : ∀ i, π i) :
  𝓝[pi I s] x = (⨅ i ∈ I, comap (fun x => x i) (𝓝[s i] x i)) ⊓ ⨅ (i) (_ : i ∉ I), comap (fun x => x i) (𝓝 (x i))

Full source

theorem nhdsWithin_pi_eq {I : Set ι} (hI : I.Finite) (s : ∀ i, Set (π i)) (x : ∀ i, π i) :
    𝓝[pi I s] x =
      (⨅ i ∈ I, comap (fun x => x i) (𝓝[s i] x i)) ⊓
        ⨅ (i) (_ : i ∉ I), comap (fun x => x i) (𝓝 (x i)) := by
  simp only [nhdsWithin, nhds_pi, Filter.pi, pi_def, ← iInf_principal_finite hI, comap_inf,
    comap_principal, eval]
  rw [iInf_split _ fun i => i ∈ I, inf_right_comm]
  simp only [iInf_inf_eq]

Neighborhood Filter Decomposition for Finite Product Sets

Informal description

For a finite index set $I \subseteq \iota$, a family of sets $s_i \subseteq \pi_i$ for each $i \in \iota$, and a point $x = (x_i)_{i \in \iota}$ in the product space $\prod_{i \in \iota} \pi_i$, the neighborhood filter within the product set $\prod_{i \in I} s_i$ at $x$ is equal to the infimum of: 1. The infimum over $i \in I$ of the pullback under the projection $\pi_i$ of the neighborhood filter within $s_i$ at $x_i$, and 2. The infimum over $i \notin I$ of the pullback under the projection $\pi_i$ of the neighborhood filter at $x_i$. In symbols: \[ \mathcal{N}_{\prod_{i \in I} s_i}(x) = \left(\bigsqcap_{i \in I} \pi_i^{-1}(\mathcal{N}_{s_i}(x_i))\right) \sqcap \left(\bigsqcap_{i \notin I} \pi_i^{-1}(\mathcal{N}(x_i))\right) \]

nhdsWithin_pi_univ_eq theorem

[Finite ι] (s : ∀ i, Set (π i)) (x : ∀ i, π i) : 𝓝[pi univ s] x = ⨅ i, comap (fun x => x i) (𝓝[s i] x i)

Full source

theorem nhdsWithin_pi_univ_eq [Finite ι] (s : ∀ i, Set (π i)) (x : ∀ i, π i) :
    𝓝[pi univ s] x = ⨅ i, comap (fun x => x i) (𝓝[s i] x i) := by
  simpa [nhdsWithin] using nhdsWithin_pi_eq finite_univ s x

Neighborhood Filter Decomposition for Finite Product Spaces over Universal Index Set

Informal description

For a finite index type $\iota$, a family of sets $s_i \subseteq \pi_i$ for each $i \in \iota$, and a point $x = (x_i)_{i \in \iota}$ in the product space $\prod_{i \in \iota} \pi_i$, the neighborhood filter within the product set $\prod_{i \in \iota} s_i$ at $x$ is equal to the infimum over all $i \in \iota$ of the pullback under the projection $\pi_i$ of the neighborhood filter within $s_i$ at $x_i$. In symbols: \[ \mathcal{N}_{\prod_{i \in \iota} s_i}(x) = \bigsqcap_{i \in \iota} \pi_i^{-1}(\mathcal{N}_{s_i}(x_i)) \]

nhdsWithin_pi_eq_bot theorem

{I : Set ι} {s : ∀ i, Set (π i)} {x : ∀ i, π i} : 𝓝[pi I s] x = ⊥ ↔ ∃ i ∈ I, 𝓝[s i] x i = ⊥

Full source

theorem nhdsWithin_pi_eq_bot {I : Set ι} {s : ∀ i, Set (π i)} {x : ∀ i, π i} :
    𝓝[pi I s] x𝓝[pi I s] x = ⊥ ↔ ∃ i ∈ I, 𝓝[s i] x i = ⊥ := by
  simp only [nhdsWithin, nhds_pi, pi_inf_principal_pi_eq_bot]

Triviality of Product Neighborhood Filter Within Subset

Informal description

For an index set $I$ and a family of sets $s_i \subseteq \pi_i$ for each $i \in I$, the neighborhood filter within the product set $\prod_{i \in I} s_i$ at a point $x$ is trivial (equal to $\bot$) if and only if there exists some index $i \in I$ such that the neighborhood filter within $s_i$ at $x_i$ is trivial.

nhdsWithin_pi_neBot theorem

{I : Set ι} {s : ∀ i, Set (π i)} {x : ∀ i, π i} : (𝓝[pi I s] x).NeBot ↔ ∀ i ∈ I, (𝓝[s i] x i).NeBot

Full source

theorem nhdsWithin_pi_neBot {I : Set ι} {s : ∀ i, Set (π i)} {x : ∀ i, π i} :
    (𝓝[pi I s] x).NeBot ↔ ∀ i ∈ I, (𝓝[s i] x i).NeBot := by
  simp [neBot_iff, nhdsWithin_pi_eq_bot]

Non-triviality of Product Neighborhood Filter Within Subsets

Informal description

For an index set $I$ and a family of sets $s_i \subseteq \pi_i$ for each $i \in I$, the neighborhood filter within the product set $\prod_{i \in I} s_i$ at a point $x = (x_i)_{i \in I}$ is non-trivial if and only if for every $i \in I$, the neighborhood filter within $s_i$ at $x_i$ is non-trivial.

instNeBotNhdsWithinUnivPi instance

{s : ∀ i, Set (π i)} {x : ∀ i, π i} [∀ i, (𝓝[s i] x i).NeBot] : (𝓝[pi univ s] x).NeBot

Full source

instance instNeBotNhdsWithinUnivPi {s : ∀ i, Set (π i)} {x : ∀ i, π i}
    [∀ i, (𝓝[s i] x i).NeBot] : (𝓝[pi univ s] x).NeBot := by
  simpa [nhdsWithin_pi_neBot]

Non-triviality of Product Neighborhood Filters within Universal Sets

Informal description

For any family of sets $s_i \subseteq \pi_i$ indexed by $i$ and any point $x = (x_i)_i$ in the product space $\prod_i \pi_i$, if for every $i$ the neighborhood filter $\mathcal{N}[s_i] x_i$ within $s_i$ at $x_i$ is non-trivial, then the neighborhood filter $\mathcal{N}[\prod_i s_i] x$ within the product set $\prod_i s_i$ at $x$ is also non-trivial.

Pi.instNeBotNhdsWithinIio instance

[Nonempty ι] [∀ i, Preorder (π i)] {x : ∀ i, π i} [∀ i, (𝓝[<] x i).NeBot] : (𝓝[<] x).NeBot

Full source

instance Pi.instNeBotNhdsWithinIio [Nonempty ι] [∀ i, Preorder (π i)] {x : ∀ i, π i}
    [∀ i, (𝓝[<] x i).NeBot] : (𝓝[<] x).NeBot :=
  have : (𝓝[pi univ fun i ↦ Iio (x i)] x).NeBot := inferInstance
  this.mono <| nhdsWithin_mono _ fun _y hy ↦ lt_of_strongLT fun i ↦ hy i trivial

Non-triviality of Product Neighborhood Filter within Left-infinite Intervals

Informal description

For a nonempty index set $\iota$ and a family of preorders $(\pi_i)_{i \in \iota}$, given a point $x = (x_i)_{i \in \iota}$ in the product space $\prod_{i} \pi_i$, if for each $i$ the neighborhood filter $\mathcal{N}[<] x_i$ at $x_i$ within the left-infinite interval $(-\infty, x_i)$ is non-trivial, then the neighborhood filter $\mathcal{N}[<] x$ at $x$ within the product of left-infinite intervals $\prod_{i} (-\infty, x_i)$ is also non-trivial.

Pi.instNeBotNhdsWithinIoi instance

[Nonempty ι] [∀ i, Preorder (π i)] {x : ∀ i, π i} [∀ i, (𝓝[>] x i).NeBot] : (𝓝[>] x).NeBot

Full source

instance Pi.instNeBotNhdsWithinIoi [Nonempty ι] [∀ i, Preorder (π i)] {x : ∀ i, π i}
    [∀ i, (𝓝[>] x i).NeBot] : (𝓝[>] x).NeBot :=
  Pi.instNeBotNhdsWithinIio (π := fun i ↦ (π i)ᵒᵈ) (x := fun i ↦ OrderDual.toDual (x i))

Non-triviality of Product Neighborhood Filter within Right-infinite Intervals

Informal description

For a nonempty index set $\iota$ and a family of preorders $(\pi_i)_{i \in \iota}$, given a point $x = (x_i)_{i \in \iota}$ in the product space $\prod_{i} \pi_i$, if for each $i$ the neighborhood filter $\mathcal{N}[>] x_i$ at $x_i$ within the right-infinite interval $(x_i, \infty)$ is non-trivial, then the neighborhood filter $\mathcal{N}[>] x$ at $x$ within the product of right-infinite intervals $\prod_{i} (x_i, \infty)$ is also non-trivial.

Filter.Tendsto.piecewise_nhdsWithin theorem

 {f g : α → β} {t : Set α} [∀ x, Decidable (x ∈ t)] {a : α} {s : Set α} {l : Filter β} (h₀ : Tendsto f (𝓝[s ∩ t] a) l)
  (h₁ : Tendsto g (𝓝[s ∩ tᶜ] a) l) : Tendsto (piecewise t f g) (𝓝[s] a) l

Full source

theorem Filter.Tendsto.piecewise_nhdsWithin {f g : α → β} {t : Set α} [∀ x, Decidable (x ∈ t)]
    {a : α} {s : Set α} {l : Filter β} (h₀ : Tendsto f (𝓝[s ∩ t] a) l)
    (h₁ : Tendsto g (𝓝[s ∩ tᶜ] a) l) : Tendsto (piecewise t f g) (𝓝[s] a) l := by
  apply Tendsto.piecewise <;> rwa [← nhdsWithin_inter']

Limit of Piecewise Function Along Relative Neighborhood Filter

Informal description

Let $f, g : \alpha \to \beta$ be functions, $t \subseteq \alpha$ a subset with decidable membership, $a \in \alpha$ a point, $s \subseteq \alpha$ a subset, and $l$ a filter on $\beta$. If $f$ tends to $l$ along the neighborhood filter of $a$ within $s \cap t$, and $g$ tends to $l$ along the neighborhood filter of $a$ within $s \cap t^c$, then the piecewise function $t.\text{piecewise}\ f\ g$ tends to $l$ along the neighborhood filter of $a$ within $s$.

Filter.Tendsto.if_nhdsWithin theorem

 {f g : α → β} {p : α → Prop} [DecidablePred p] {a : α} {s : Set α} {l : Filter β}
  (h₀ : Tendsto f (𝓝[s ∩ {x | p x}] a) l) (h₁ : Tendsto g (𝓝[s ∩ {x | ¬p x}] a) l) :
  Tendsto (fun x => if p x then f x else g x) (𝓝[s] a) l

Full source

theorem Filter.Tendsto.if_nhdsWithin {f g : α → β} {p : α → Prop} [DecidablePred p] {a : α}
    {s : Set α} {l : Filter β} (h₀ : Tendsto f (𝓝[s ∩ { x | p x }] a) l)
    (h₁ : Tendsto g (𝓝[s ∩ { x | ¬p x }] a) l) :
    Tendsto (fun x => if p x then f x else g x) (𝓝[s] a) l :=
  h₀.piecewise_nhdsWithin h₁

Limit of Conditional Function Along Relative Neighborhood Filter

Informal description

Let $f, g : \alpha \to \beta$ be functions, $p : \alpha \to \text{Prop}$ a decidable predicate, $a \in \alpha$ a point, $s \subseteq \alpha$ a subset, and $l$ a filter on $\beta$. If $f$ tends to $l$ along the neighborhood filter of $a$ within $s \cap \{x \mid p(x)\}$, and $g$ tends to $l$ along the neighborhood filter of $a$ within $s \cap \{x \mid \neg p(x)\}$, then the function defined by $x \mapsto \text{if } p(x) \text{ then } f(x) \text{ else } g(x)$ tends to $l$ along the neighborhood filter of $a$ within $s$.

map_nhdsWithin theorem

 (f : α → β) (a : α) (s : Set α) : map f (𝓝[s] a) = ⨅ t ∈ {t : Set α | a ∈ t ∧ IsOpen t}, 𝓟 (f '' (t ∩ s))

Full source

theorem map_nhdsWithin (f : α → β) (a : α) (s : Set α) :
    map f (𝓝[s] a) = ⨅ t ∈ { t : Set α | a ∈ t ∧ IsOpen t }, 𝓟 (f '' (t ∩ s)) :=
  ((nhdsWithin_basis_open a s).map f).eq_biInf

Image of Relative Neighborhood Filter under Continuous Function

Informal description

Let $f : \alpha \to \beta$ be a function between topological spaces, $a \in \alpha$ a point, and $s \subseteq \alpha$ a subset. The image under $f$ of the neighborhood filter of $a$ within $s$ is equal to the infimum of the principal filters of the images $f(u \cap s)$, where $u$ ranges over all open sets containing $a$.

tendsto_nhdsWithin_mono_left theorem

 {f : α → β} {a : α} {s t : Set α} {l : Filter β} (hst : s ⊆ t) (h : Tendsto f (𝓝[t] a) l) : Tendsto f (𝓝[s] a) l

Full source

theorem tendsto_nhdsWithin_mono_left {f : α → β} {a : α} {s t : Set α} {l : Filter β} (hst : s ⊆ t)
    (h : Tendsto f (𝓝[t] a) l) : Tendsto f (𝓝[s] a) l :=
  h.mono_left <| nhdsWithin_mono a hst

Monotonicity of Tendency with Respect to Neighborhood Subsets

Informal description

Let $f : \alpha \to \beta$ be a function, $a \in \alpha$ a point, and $s, t \subseteq \alpha$ subsets with $s \subseteq t$. If $f$ tends to a filter $l$ along the neighborhood filter of $a$ within $t$, then $f$ also tends to $l$ along the neighborhood filter of $a$ within $s$.

tendsto_nhdsWithin_mono_right theorem

 {f : β → α} {l : Filter β} {a : α} {s t : Set α} (hst : s ⊆ t) (h : Tendsto f l (𝓝[s] a)) : Tendsto f l (𝓝[t] a)

Full source

theorem tendsto_nhdsWithin_mono_right {f : β → α} {l : Filter β} {a : α} {s t : Set α} (hst : s ⊆ t)
    (h : Tendsto f l (𝓝[s] a)) : Tendsto f l (𝓝[t] a) :=
  h.mono_right (nhdsWithin_mono a hst)

Monotonicity of Tendency with Respect to Larger Neighborhoods

Informal description

Let $f : \beta \to \alpha$ be a function, $l$ a filter on $\beta$, and $a \in \alpha$ with subsets $s \subseteq t \subseteq \alpha$. If $f$ tends to the neighborhood filter of $a$ within $s$ along $l$, then $f$ also tends to the neighborhood filter of $a$ within $t$ along $l$.

tendsto_nhdsWithin_of_tendsto_nhds theorem

{f : α → β} {a : α} {s : Set α} {l : Filter β} (h : Tendsto f (𝓝 a) l) : Tendsto f (𝓝[s] a) l

Full source

theorem tendsto_nhdsWithin_of_tendsto_nhds {f : α → β} {a : α} {s : Set α} {l : Filter β}
    (h : Tendsto f (𝓝 a) l) : Tendsto f (𝓝[s] a) l :=
  h.mono_left inf_le_left

Convergence in Neighborhood Implies Convergence in Restricted Neighborhood

Informal description

Let $f : \alpha \to \beta$ be a function, $a \in \alpha$ a point, $s \subseteq \alpha$ a subset, and $l$ a filter on $\beta$. If $f$ tends to $l$ along the neighborhood filter of $a$, then $f$ also tends to $l$ along the neighborhood filter of $a$ within $s$.

eventually_mem_of_tendsto_nhdsWithin theorem

{f : β → α} {a : α} {s : Set α} {l : Filter β} (h : Tendsto f l (𝓝[s] a)) : ∀ᶠ i in l, f i ∈ s

Full source

theorem eventually_mem_of_tendsto_nhdsWithin {f : β → α} {a : α} {s : Set α} {l : Filter β}
    (h : Tendsto f l (𝓝[s] a)) : ∀ᶠ i in l, f i ∈ s := by
  simp_rw [nhdsWithin_eq, tendsto_iInf, mem_setOf_eq, tendsto_principal, mem_inter_iff,
    eventually_and] at h
  exact (h univ ⟨mem_univ a, isOpen_univ⟩).2

Eventual Membership in Set Under Convergence Within Subset

Informal description

For any function $f : \beta \to \alpha$, point $a \in \alpha$, subset $s \subseteq \alpha$, and filter $l$ on $\beta$, if $f$ tends to the neighborhood filter of $a$ within $s$ along $l$, then eventually for all $i$ in $l$, $f(i)$ belongs to $s$.

tendsto_nhds_of_tendsto_nhdsWithin theorem

{f : β → α} {a : α} {s : Set α} {l : Filter β} (h : Tendsto f l (𝓝[s] a)) : Tendsto f l (𝓝 a)

Full source

theorem tendsto_nhds_of_tendsto_nhdsWithin {f : β → α} {a : α} {s : Set α} {l : Filter β}
    (h : Tendsto f l (𝓝[s] a)) : Tendsto f l (𝓝 a) :=
  h.mono_right nhdsWithin_le_nhds

Convergence within subset implies global convergence

Informal description

Let $f : \beta \to \alpha$ be a function between topological spaces, $a \in \alpha$ a point, $s \subseteq \alpha$ a subset, and $l$ a filter on $\beta$. If $f$ tends to $a$ along the neighborhood filter of $a$ within $s$ (i.e., $\lim_{l} f \in \mathcal{N}_s(a)$), then $f$ tends to $a$ along the ordinary neighborhood filter of $a$ (i.e., $\lim_{l} f \in \mathcal{N}(a)$).

nhdsWithin_neBot_of_mem theorem

{s : Set α} {x : α} (hx : x ∈ s) : NeBot (𝓝[s] x)

Full source

theorem nhdsWithin_neBot_of_mem {s : Set α} {x : α} (hx : x ∈ s) : NeBot (𝓝[s] x) :=
  mem_closure_iff_nhdsWithin_neBot.1 <| subset_closure hx

Non-triviality of Neighborhood Filter Within a Set at a Member Point

Informal description

For any set $s$ in a topological space and any point $x \in s$, the neighborhood filter $\mathcal{N}_s(x)$ (the filter of neighborhoods of $x$ within $s$) is non-trivial (i.e., it does not contain the empty set).

IsClosed.mem_of_nhdsWithin_neBot theorem

{s : Set α} (hs : IsClosed s) {x : α} (hx : NeBot <| 𝓝[s] x) : x ∈ s

Full source

theorem IsClosed.mem_of_nhdsWithin_neBot {s : Set α} (hs : IsClosed s) {x : α}
    (hx : NeBot <| 𝓝[s] x) : x ∈ s :=
  hs.closure_eq ▸ mem_closure_iff_nhdsWithin_neBot.2 hx

Closed Set Membership via Non-trivial Neighborhood Filter Within Set

Informal description

Let $s$ be a closed subset of a topological space $\alpha$ and $x$ a point in $\alpha$. If the neighborhood filter of $x$ within $s$ is non-trivial (i.e., $\mathcal{N}_s(x)$ is not the trivial filter), then $x$ must belong to $s$.

DenseRange.nhdsWithin_neBot theorem

{ι : Type*} {f : ι → α} (h : DenseRange f) (x : α) : NeBot (𝓝[range f] x)

Full source

theorem DenseRange.nhdsWithin_neBot {ι : Type*} {f : ι → α} (h : DenseRange f) (x : α) :
    NeBot (𝓝[range f] x) :=
  mem_closure_iff_clusterPt.1 (h x)

Non-triviality of Neighborhood Filter Within the Range of a Dense Function

Informal description

For any topological space $\alpha$ and any dense range function $f \colon \iota \to \alpha$, the neighborhood filter of any point $x \in \alpha$ within the range of $f$ is non-trivial. That is, $\mathcal{N}_{\text{range } f}(x)$ is not the trivial filter.

mem_closure_pi theorem

 {ι : Type*} {α : ι → Type*} [∀ i, TopologicalSpace (α i)] {I : Set ι} {s : ∀ i, Set (α i)} {x : ∀ i, α i} :
  x ∈ closure (pi I s) ↔ ∀ i ∈ I, x i ∈ closure (s i)

Full source

theorem mem_closure_pi {ι : Type*} {α : ι → Type*} [∀ i, TopologicalSpace (α i)] {I : Set ι}
    {s : ∀ i, Set (α i)} {x : ∀ i, α i} : x ∈ closure (pi I s)x ∈ closure (pi I s) ↔ ∀ i ∈ I, x i ∈ closure (s i) := by
  simp only [mem_closure_iff_nhdsWithin_neBot, nhdsWithin_pi_neBot]

Characterization of Points in the Closure of a Restricted Product Set

Informal description

Let $\{α_i\}_{i \in \iota}$ be a family of topological spaces, $I \subseteq \iota$ a subset of indices, and $s_i \subseteq α_i$ subsets for each $i \in I$. For a point $x = (x_i)_{i \in \iota}$ in the product space $\prod_{i \in \iota} α_i$, the following are equivalent: 1. $x$ belongs to the closure of the restricted product $\prod_{i \in I} s_i$ (where $s_i = α_i$ for $i \notin I$). 2. For each $i \in I$, the component $x_i$ belongs to the closure of $s_i$ in $α_i$.

closure_pi_set theorem

 {ι : Type*} {α : ι → Type*} [∀ i, TopologicalSpace (α i)] (I : Set ι) (s : ∀ i, Set (α i)) :
  closure (pi I s) = pi I fun i => closure (s i)

Full source

theorem closure_pi_set {ι : Type*} {α : ι → Type*} [∀ i, TopologicalSpace (α i)] (I : Set ι)
    (s : ∀ i, Set (α i)) : closure (pi I s) = pi I fun i => closure (s i) :=
  Set.ext fun _ => mem_closure_pi

Closure of Restricted Product Set Equals Product of Closures

Informal description

Let $\{α_i\}_{i \in \iota}$ be a family of topological spaces, $I \subseteq \iota$ a subset of indices, and $s_i \subseteq α_i$ subsets for each $i \in \iota$. The closure of the restricted product set $\prod_{i \in I} s_i$ (where $s_i = α_i$ for $i \notin I$) is equal to the product $\prod_{i \in I} \overline{s_i}$, where $\overline{s_i}$ denotes the closure of $s_i$ in $α_i$.

dense_pi theorem

 {ι : Type*} {α : ι → Type*} [∀ i, TopologicalSpace (α i)] {s : ∀ i, Set (α i)} (I : Set ι)
  (hs : ∀ i ∈ I, Dense (s i)) : Dense (pi I s)

Full source

theorem dense_pi {ι : Type*} {α : ι → Type*} [∀ i, TopologicalSpace (α i)] {s : ∀ i, Set (α i)}
    (I : Set ι) (hs : ∀ i ∈ I, Dense (s i)) : Dense (pi I s) := by
  simp only [dense_iff_closure_eq, closure_pi_set, pi_congr rfl fun i hi => (hs i hi).closure_eq,
    pi_univ]

Density of Restricted Product of Dense Sets

Informal description

Let $\{α_i\}_{i \in \iota}$ be a family of topological spaces, $I \subseteq \iota$ a subset of indices, and $s_i \subseteq α_i$ subsets such that each $s_i$ is dense in $α_i$ for $i \in I$. Then the restricted product set $\prod_{i \in I} s_i$ (where $s_i = α_i$ for $i \notin I$) is dense in the product space $\prod_{i \in \iota} α_i$.

DenseRange.piMap theorem

 {ι : Type*} {X Y : ι → Type*} [∀ i, TopologicalSpace (Y i)] {f : (i : ι) → (X i) → (Y i)}
  (hf : ∀ i, DenseRange (f i)) : DenseRange (Pi.map f)

Full source

theorem DenseRange.piMap {ι : Type*} {X Y : ι → Type*} [∀ i, TopologicalSpace (Y i)]
    {f : (i : ι) → (X i) → (Y i)} (hf : ∀ i, DenseRange (f i)):
    DenseRange (Pi.map f) := by
  rw [DenseRange, Set.range_piMap]
  exact dense_pi Set.univ (fun i _ => hf i)

Density of Component-wise Mapping in Product Space

Informal description

Let $\{X_i\}_{i \in \iota}$ and $\{Y_i\}_{i \in \iota}$ be families of types, with each $Y_i$ equipped with a topological space structure. Given a family of functions $f_i : X_i \to Y_i$ such that each $f_i$ has dense range in $Y_i$, the component-wise application function $\text{Pi.map} \, f$ (which maps $(x_i)_{i \in \iota}$ to $(f_i(x_i))_{i \in \iota}$) has dense range in the product space $\prod_{i \in \iota} Y_i$.

eventuallyEq_nhdsWithin_iff theorem

{f g : α → β} {s : Set α} {a : α} : f =ᶠ[𝓝[s] a] g ↔ ∀ᶠ x in 𝓝 a, x ∈ s → f x = g x

Full source

theorem eventuallyEq_nhdsWithin_iff {f g : α → β} {s : Set α} {a : α} :
    f =ᶠ[𝓝[s] a] gf =ᶠ[𝓝[s] a] g ↔ ∀ᶠ x in 𝓝 a, x ∈ s → f x = g x :=
  mem_inf_principal

Characterization of Eventual Equality in Restricted Neighborhoods

Informal description

For functions $f, g : \alpha \to \beta$, a set $s \subseteq \alpha$, and a point $a \in \alpha$, the following are equivalent: 1. $f$ and $g$ are eventually equal in the neighborhood filter of $a$ restricted to $s$ (i.e., $f = g$ for all $x$ sufficiently close to $a$ within $s$) 2. For all $x$ sufficiently close to $a$, if $x \in s$ then $f(x) = g(x)$.

eventuallyEq_nhds_of_eventuallyEq_nhdsNE theorem

{f g : α → β} {a : α} (h₁ : f =ᶠ[𝓝[≠] a] g) (h₂ : f a = g a) : f =ᶠ[𝓝 a] g

Full source

/-- Two functions agree on a neighborhood of `x` if they agree at `x` and in a punctured
neighborhood. -/
theorem eventuallyEq_nhds_of_eventuallyEq_nhdsNE {f g : α → β} {a : α} (h₁ : f =ᶠ[𝓝[≠] a] g)
    (h₂ : f a = g a) :
    f =ᶠ[𝓝 a] g := by
  filter_upwards [eventually_nhdsWithin_iff.1 h₁]
  intro x hx
  by_cases h₂x : x = a
  · simp [h₂x, h₂]
  · tauto

Agreement on Punctured Neighborhood and Point Implies Local Agreement

Informal description

Let $f, g : \alpha \to \beta$ be functions and $a \in \alpha$ a point in a topological space. If: 1. $f$ and $g$ agree on a punctured neighborhood of $a$ (i.e., $f = g$ for all $x$ sufficiently close to but not equal to $a$), and 2. $f(a) = g(a)$, then $f$ and $g$ agree on a full neighborhood of $a$.

eventuallyEq_nhdsWithin_of_eqOn theorem

{f g : α → β} {s : Set α} {a : α} (h : EqOn f g s) : f =ᶠ[𝓝[s] a] g

Full source

theorem eventuallyEq_nhdsWithin_of_eqOn {f g : α → β} {s : Set α} {a : α} (h : EqOn f g s) :
    f =ᶠ[𝓝[s] a] g :=
  mem_inf_of_right h

Agreement on Set Implies Local Agreement in Relative Neighborhoods

Informal description

Let $f, g : \alpha \to \beta$ be functions, $s \subseteq \alpha$ a subset, and $a \in \alpha$ a point. If $f$ and $g$ agree on $s$ (i.e., $f(x) = g(x)$ for all $x \in s$), then $f$ and $g$ are eventually equal in the neighborhood filter of $a$ restricted to $s$. In other words, if $f|_s = g|_s$, then $f = g$ eventually in $\mathcal{N}_s(a)$.

Set.EqOn.eventuallyEq_nhdsWithin theorem

{f g : α → β} {s : Set α} {a : α} (h : EqOn f g s) : f =ᶠ[𝓝[s] a] g

Full source

theorem Set.EqOn.eventuallyEq_nhdsWithin {f g : α → β} {s : Set α} {a : α} (h : EqOn f g s) :
    f =ᶠ[𝓝[s] a] g :=
  eventuallyEq_nhdsWithin_of_eqOn h

Agreement on Set Implies Local Agreement in Relative Neighborhoods

Informal description

Let $f, g : \alpha \to \beta$ be functions, $s \subseteq \alpha$ a subset, and $a \in \alpha$ a point. If $f$ and $g$ agree on $s$ (i.e., $f(x) = g(x)$ for all $x \in s$), then $f$ and $g$ are eventually equal in the neighborhood filter of $a$ restricted to $s$. In other words, if $f|_s = g|_s$, then $f = g$ eventually in $\mathcal{N}_s(a)$.

tendsto_nhdsWithin_congr theorem

 {f g : α → β} {s : Set α} {a : α} {l : Filter β} (hfg : ∀ x ∈ s, f x = g x) (hf : Tendsto f (𝓝[s] a) l) :
  Tendsto g (𝓝[s] a) l

Full source

theorem tendsto_nhdsWithin_congr {f g : α → β} {s : Set α} {a : α} {l : Filter β}
    (hfg : ∀ x ∈ s, f x = g x) (hf : Tendsto f (𝓝[s] a) l) : Tendsto g (𝓝[s] a) l :=
  (tendsto_congr' <| eventuallyEq_nhdsWithin_of_eqOn hfg).1 hf

Limit Congruence for Functions Agreeing on a Set

Informal description

Let $f, g : \alpha \to \beta$ be functions, $s \subseteq \alpha$ a subset, $a \in \alpha$ a point, and $l$ a filter on $\beta$. If $f$ and $g$ agree on $s$ (i.e., $f(x) = g(x)$ for all $x \in s$) and $f$ tends to $l$ along the neighborhood filter of $a$ restricted to $s$, then $g$ also tends to $l$ along the same restricted neighborhood filter. In other words, if $f|_s = g|_s$ and $\lim_{x \to a, x \in s} f(x) = l$, then $\lim_{x \to a, x \in s} g(x) = l$.

eventually_nhdsWithin_of_forall theorem

{s : Set α} {a : α} {p : α → Prop} (h : ∀ x ∈ s, p x) : ∀ᶠ x in 𝓝[s] a, p x

Full source

theorem eventually_nhdsWithin_of_forall {s : Set α} {a : α} {p : α → Prop} (h : ∀ x ∈ s, p x) :
    ∀ᶠ x in 𝓝[s] a, p x :=
  mem_inf_of_right h

Eventual Truth of Predicate in Neighborhood Within a Set

Informal description

For any set $s$ in a topological space $\alpha$, any point $a \in \alpha$, and any predicate $p$ on $\alpha$, if $p(x)$ holds for all $x \in s$, then $p(x)$ holds for all $x$ in some neighborhood of $a$ within $s$. In other words, the predicate $p$ is eventually true in the neighborhood filter $\mathcal{N}[s] a$.

tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within theorem

 {a : α} {l : Filter β} {s : Set α} (f : β → α) (h1 : Tendsto f l (𝓝 a)) (h2 : ∀ᶠ x in l, f x ∈ s) :
  Tendsto f l (𝓝[s] a)

Full source

theorem tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within {a : α} {l : Filter β} {s : Set α}
    (f : β → α) (h1 : Tendsto f l (𝓝 a)) (h2 : ∀ᶠ x in l, f x ∈ s) : Tendsto f l (𝓝[s] a) :=
  tendsto_inf.2 ⟨h1, tendsto_principal.2 h2⟩

Limit within a subset via limit and eventual membership

Informal description

Let $f : \beta \to \alpha$ be a function between topological spaces, $a \in \alpha$, $s \subseteq \alpha$, and $l$ a filter on $\beta$. If $f$ tends to $a$ along $l$ (i.e., $\lim_{x \to l} f(x) = a$) and eventually all values of $f$ lie in $s$ (i.e., $\{x \mid f(x) \in s\} \in l$), then $f$ tends to $a$ within $s$ along $l$ (i.e., $\lim_{x \to l, f(x) \in s} f(x) = a$).

tendsto_nhdsWithin_iff theorem

 {a : α} {l : Filter β} {s : Set α} {f : β → α} : Tendsto f l (𝓝[s] a) ↔ Tendsto f l (𝓝 a) ∧ ∀ᶠ n in l, f n ∈ s

Full source

theorem tendsto_nhdsWithin_iff {a : α} {l : Filter β} {s : Set α} {f : β → α} :
    TendstoTendsto f l (𝓝[s] a) ↔ Tendsto f l (𝓝 a) ∧ ∀ᶠ n in l, f n ∈ s :=
  ⟨fun h => ⟨tendsto_nhds_of_tendsto_nhdsWithin h, eventually_mem_of_tendsto_nhdsWithin h⟩, fun h =>
    tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ h.1 h.2⟩

Characterization of Convergence within a Subset via Global Convergence and Eventual Membership

Informal description

For a function $f : \beta \to \alpha$ between topological spaces, a point $a \in \alpha$, a subset $s \subseteq \alpha$, and a filter $l$ on $\beta$, the following are equivalent: 1. $f$ tends to $a$ along the neighborhood filter of $a$ within $s$ (i.e., $\lim_{x \to l} f(x) = a$ within $s$). 2. $f$ tends to $a$ along the ordinary neighborhood filter of $a$ (i.e., $\lim_{x \to l} f(x) = a$) and eventually all values of $f$ lie in $s$ (i.e., $\{x \mid f(x) \in s\} \in l$).

tendsto_nhdsWithin_range theorem

{a : α} {l : Filter β} {f : β → α} : Tendsto f l (𝓝[range f] a) ↔ Tendsto f l (𝓝 a)

Full source

@[simp]
theorem tendsto_nhdsWithin_range {a : α} {l : Filter β} {f : β → α} :
    TendstoTendsto f l (𝓝[range f] a) ↔ Tendsto f l (𝓝 a) :=
  ⟨fun h => h.mono_right inf_le_left, fun h =>
    tendsto_inf.2 ⟨h, tendsto_principal.2 <| Eventually.of_forall mem_range_self⟩⟩

Limit within Range Equals Limit in Whole Space

Informal description

For a function $f : \beta \to \alpha$ between topological spaces, a point $a \in \alpha$, and a filter $l$ on $\beta$, the following are equivalent: 1. $f$ tends to $a$ along $l$ within the range of $f$ (i.e., $\lim_{x \to l, f(x) \in \text{range } f} f(x) = a$). 2. $f$ tends to $a$ along $l$ (i.e., $\lim_{x \to l} f(x) = a$).

eventually_nhdsWithin_of_eventually_nhds theorem

{s : Set α} {a : α} {p : α → Prop} (h : ∀ᶠ x in 𝓝 a, p x) : ∀ᶠ x in 𝓝[s] a, p x

Full source

theorem eventually_nhdsWithin_of_eventually_nhds {s : Set α}
    {a : α} {p : α → Prop} (h : ∀ᶠ x in 𝓝 a, p x) : ∀ᶠ x in 𝓝[s] a, p x :=
  mem_nhdsWithin_of_mem_nhds h

Neighborhood Restriction Preserves Eventual Properties

Informal description

For any set $s$ in a topological space $\alpha$, any point $a \in \alpha$, and any predicate $p : \alpha \to \text{Prop}$, if $p(x)$ holds for all $x$ in some neighborhood of $a$, then $p(x)$ also holds for all $x$ in the neighborhood of $a$ within $s$.

Set.MapsTo.preimage_mem_nhdsWithin theorem

{f : α → β} {s : Set α} {t : Set β} {x : α} (hst : MapsTo f s t) : f ⁻¹' t ∈ 𝓝[s] x

Full source

lemma Set.MapsTo.preimage_mem_nhdsWithin {f : α → β} {s : Set α} {t : Set β} {x : α}
    (hst : MapsTo f s t) : f ⁻¹' tf ⁻¹' t ∈ 𝓝[s] x :=
  Filter.mem_of_superset self_mem_nhdsWithin hst

Preimage of Target is Neighborhood When Function Maps Subset

Informal description

Let $f : \alpha \to \beta$ be a function between topological spaces, $s \subseteq \alpha$, $t \subseteq \beta$, and $x \in \alpha$. If $f$ maps $s$ into $t$ (i.e., $f(s) \subseteq t$), then the preimage $f^{-1}(t)$ is a neighborhood of $x$ within $s$.

mem_nhdsWithin_subtype theorem

 {s : Set α} {a : { x // x ∈ s }} {t u : Set { x // x ∈ s }} : t ∈ 𝓝[u] a ↔ t ∈ comap ((↑) : s → α) (𝓝[(↑) '' u] a)

Full source

theorem mem_nhdsWithin_subtype {s : Set α} {a : { x // x ∈ s }} {t u : Set { x // x ∈ s }} :
    t ∈ 𝓝[u] at ∈ 𝓝[u] a ↔ t ∈ comap ((↑) : s → α) (𝓝[(↑) '' u] a) := by
  rw [nhdsWithin, nhds_subtype, principal_subtype, ← comap_inf, ← nhdsWithin]

Characterization of Neighborhoods in Subspace Topology via Inclusion Map

Informal description

Let $s$ be a subset of a topological space $\alpha$, and let $a$ be an element of $s$ (viewed as a point in the subtype $\{x \in \alpha \mid x \in s\}$). For any subsets $t$ and $u$ of this subtype, the following are equivalent: 1. $t$ is a neighborhood of $a$ within $u$ in the subspace topology of $s$ 2. $t$ belongs to the preimage of the neighborhood filter of $a$ (as an element of $\alpha$) within the image of $u$ under the inclusion map $\iota : s \hookrightarrow \alpha$ In other words, $t \in \mathcal{N}_u(a)$ (subspace topology) if and only if $t \in \iota^{-1}(\mathcal{N}_{\iota(u)}(\iota(a)))$ where $\iota$ is the inclusion map and $\mathcal{N}$ denotes neighborhood filters.

nhdsWithin_subtype theorem

 (s : Set α) (a : { x // x ∈ s }) (t : Set { x // x ∈ s }) : 𝓝[t] a = comap ((↑) : s → α) (𝓝[(↑) '' t] a)

Full source

theorem nhdsWithin_subtype (s : Set α) (a : { x // x ∈ s }) (t : Set { x // x ∈ s }) :
    𝓝[t] a = comap ((↑) : s → α) (𝓝[(↑) '' t] a) :=
  Filter.ext fun _ => mem_nhdsWithin_subtype

Neighborhood Filter in Subspace Topology via Preimage of Inclusion Map

Informal description

Let $s$ be a subset of a topological space $\alpha$, and let $a$ be an element of $s$ (viewed as a point in the subtype $\{x \in \alpha \mid x \in s\}$). For any subset $t$ of this subtype, the neighborhood filter of $a$ within $t$ in the subspace topology of $s$ is equal to the preimage under the inclusion map $\iota : s \hookrightarrow \alpha$ of the neighborhood filter of $a$ (as an element of $\alpha$) within the image $\iota(t)$. In other words, $\mathcal{N}_t(a) = \iota^{-1}(\mathcal{N}_{\iota(t)}(\iota(a)))$, where $\mathcal{N}$ denotes neighborhood filters and $\iota$ is the inclusion map.

nhdsWithin_eq_map_subtype_coe theorem

{s : Set α} {a : α} (h : a ∈ s) : 𝓝[s] a = map ((↑) : s → α) (𝓝 ⟨a, h⟩)

Full source

theorem nhdsWithin_eq_map_subtype_coe {s : Set α} {a : α} (h : a ∈ s) :
    𝓝[s] a = map ((↑) : s → α) (𝓝 ⟨a, h⟩) :=
  (map_nhds_subtype_val ⟨a, h⟩).symm

Neighborhood Filter Within Subset as Image of Subspace Filter

Informal description

For any subset $s$ of a topological space $\alpha$ and any point $a \in s$, the neighborhood filter of $a$ within $s$ (denoted $\mathcal{N}_s(a)$) is equal to the image under the inclusion map $\iota : s \to \alpha$ of the neighborhood filter of the point $\langle a, h\rangle$ in the subspace topology of $s$, where $h$ is the proof that $a \in s$.

mem_nhds_subtype_iff_nhdsWithin theorem

{s : Set α} {a : s} {t : Set s} : t ∈ 𝓝 a ↔ (↑) '' t ∈ 𝓝[s] (a : α)

Full source

theorem mem_nhds_subtype_iff_nhdsWithin {s : Set α} {a : s} {t : Set s} :
    t ∈ 𝓝 at ∈ 𝓝 a ↔ (↑) '' t ∈ 𝓝[s] (a : α) := by
  rw [← map_nhds_subtype_val, image_mem_map_iff Subtype.val_injective]

Neighborhood Criterion in Subspace Topology via Inclusion Map

Informal description

Let $s$ be a subset of a topological space $\alpha$, and let $a$ be an element of $s$. For any subset $t$ of $s$, $t$ is a neighborhood of $a$ in the subspace topology of $s$ if and only if the image of $t$ under the inclusion map from $s$ to $\alpha$ is a neighborhood of $a$ within $s$ in $\alpha$.

preimage_coe_mem_nhds_subtype theorem

{s t : Set α} {a : s} : (↑) ⁻¹' t ∈ 𝓝 a ↔ t ∈ 𝓝[s] ↑a

Full source

theorem preimage_coe_mem_nhds_subtype {s t : Set α} {a : s} : (↑) ⁻¹' t(↑) ⁻¹' t ∈ 𝓝 a(↑) ⁻¹' t ∈ 𝓝 a ↔ t ∈ 𝓝[s] ↑a := by
  rw [← map_nhds_subtype_val, mem_map]

Preimage of Neighborhood under Inclusion Map in Subspace Topology

Informal description

Let $s$ and $t$ be subsets of a topological space $\alpha$, and let $a$ be a point in $s$. Then the preimage of $t$ under the inclusion map $\iota : s \to \alpha$ is a neighborhood of $a$ in the subspace topology of $s$ if and only if $t$ is a neighborhood of $\iota(a)$ in $\alpha$ relative to $s$.

eventually_nhds_subtype_iff theorem

(s : Set α) (a : s) (P : α → Prop) : (∀ᶠ x : s in 𝓝 a, P x) ↔ ∀ᶠ x in 𝓝[s] a, P x

Full source

theorem eventually_nhds_subtype_iff (s : Set α) (a : s) (P : α → Prop) :
    (∀ᶠ x : s in 𝓝 a, P x) ↔ ∀ᶠ x in 𝓝[s] a, P x :=
  preimage_coe_mem_nhds_subtype

Equivalence of Eventual Properties in Subspace and Relative Neighborhoods

Informal description

Let $s$ be a subset of a topological space $\alpha$, and let $a$ be a point in $s$. For any predicate $P$ on $\alpha$, the following are equivalent: 1. $P(x)$ holds for all $x$ in $s$ sufficiently close to $a$ in the subspace topology of $s$. 2. $P(x)$ holds for all $x$ in $\alpha$ sufficiently close to $a$ within $s$. In other words, $P$ holds eventually near $a$ in the subspace topology of $s$ if and only if $P$ holds eventually near $a$ within $s$ in the ambient space $\alpha$.

frequently_nhds_subtype_iff theorem

(s : Set α) (a : s) (P : α → Prop) : (∃ᶠ x : s in 𝓝 a, P x) ↔ ∃ᶠ x in 𝓝[s] a, P x

Full source

theorem frequently_nhds_subtype_iff (s : Set α) (a : s) (P : α → Prop) :
    (∃ᶠ x : s in 𝓝 a, P x) ↔ ∃ᶠ x in 𝓝[s] a, P x :=
  eventually_nhds_subtype_iff s a (¬ P ·) |>.not

Frequent Occurrence Equivalence in Subspace vs. Relative Neighborhoods

Informal description

Let $s$ be a subset of a topological space $\alpha$, and let $a$ be a point in $s$. For any predicate $P$ on $\alpha$, the following are equivalent: 1. There exists a neighborhood of $a$ in the subspace topology of $s$ such that $P(x)$ holds for frequently many $x$ in this neighborhood. 2. There exists a neighborhood of $a$ within $s$ in the ambient space $\alpha$ such that $P(x)$ holds for frequently many $x$ in this neighborhood. In other words, $P$ holds frequently near $a$ in the subspace topology of $s$ if and only if $P$ holds frequently near $a$ within $s$ in the ambient space $\alpha$.

tendsto_nhdsWithin_iff_subtype theorem

 {s : Set α} {a : α} (h : a ∈ s) (f : α → β) (l : Filter β) : Tendsto f (𝓝[s] a) l ↔ Tendsto (s.restrict f) (𝓝 ⟨a, h⟩) l

Full source

theorem tendsto_nhdsWithin_iff_subtype {s : Set α} {a : α} (h : a ∈ s) (f : α → β) (l : Filter β) :
    TendstoTendsto f (𝓝[s] a) l ↔ Tendsto (s.restrict f) (𝓝 ⟨a, h⟩) l := by
  rw [nhdsWithin_eq_map_subtype_coe h, tendsto_map'_iff]; rfl

Characterization of Limit Within Subset via Subspace Topology

Informal description

Let $s$ be a subset of a topological space $\alpha$, $a \in s$ a point, $f : \alpha \to \beta$ a function, and $l$ a filter on $\beta$. The following are equivalent: 1. The function $f$ tends to $l$ as $x$ approaches $a$ within $s$ (i.e., $\lim_{x \to a, x \in s} f(x) = l$). 2. The restriction of $f$ to $s$ tends to $l$ as $x$ approaches $\langle a, h\rangle$ in the subspace topology of $s$.

ContinuousWithinAt.tendsto theorem

(h : ContinuousWithinAt f s x) : Tendsto f (𝓝[s] x) (𝓝 (f x))

Full source

/-- If a function is continuous within `s` at `x`, then it tends to `f x` within `s` by definition.
We register this fact for use with the dot notation, especially to use `Filter.Tendsto.comp` as
`ContinuousWithinAt.comp` will have a different meaning. -/
theorem ContinuousWithinAt.tendsto (h : ContinuousWithinAt f s x) :
    Tendsto f (𝓝[s] x) (𝓝 (f x)) :=
  h

Limit of a Function Continuous Within a Subset

Informal description

If a function $f : \alpha \to \beta$ is continuous at a point $x$ within a subset $s \subseteq \alpha$, then the limit of $f$ as $y$ approaches $x$ within $s$ is equal to $f(x)$. In other words, $f(y) \to f(x)$ as $y \to x$ with $y \in s$.

continuousWithinAt_univ theorem

(f : α → β) (x : α) : ContinuousWithinAt f Set.univ x ↔ ContinuousAt f x

Full source

theorem continuousWithinAt_univ (f : α → β) (x : α) :
    ContinuousWithinAtContinuousWithinAt f Set.univ x ↔ ContinuousAt f x := by
  rw [ContinuousAt, ContinuousWithinAt, nhdsWithin_univ]

Continuity within Entire Space Equals Pointwise Continuity

Informal description

For any function $f \colon \alpha \to \beta$ between topological spaces and any point $x \in \alpha$, the function $f$ is continuous at $x$ within the entire space $\alpha$ if and only if $f$ is continuous at $x$.

continuous_iff_continuousOn_univ theorem

{f : α → β} : Continuous f ↔ ContinuousOn f univ

Full source

theorem continuous_iff_continuousOn_univ {f : α → β} : ContinuousContinuous f ↔ ContinuousOn f univ := by
  simp [continuous_iff_continuousAt, ContinuousOn, ContinuousAt, ContinuousWithinAt,
    nhdsWithin_univ]

Global Continuity is Equivalent to Continuity on the Entire Space

Informal description

A function $f \colon \alpha \to \beta$ between topological spaces is continuous if and only if it is continuous on the entire space $\alpha$.

continuousWithinAt_iff_continuousAt_restrict theorem

 (f : α → β) {x : α} {s : Set α} (h : x ∈ s) : ContinuousWithinAt f s x ↔ ContinuousAt (s.restrict f) ⟨x, h⟩

Full source

theorem continuousWithinAt_iff_continuousAt_restrict (f : α → β) {x : α} {s : Set α} (h : x ∈ s) :
    ContinuousWithinAtContinuousWithinAt f s x ↔ ContinuousAt (s.restrict f) ⟨x, h⟩ :=
  tendsto_nhdsWithin_iff_subtype h f _

Characterization of Continuity Within Subset via Subspace Topology

Informal description

Let $f : \alpha \to \beta$ be a function between topological spaces, $s \subseteq \alpha$ a subset, and $x \in s$ a point. Then $f$ is continuous at $x$ within $s$ if and only if the restriction of $f$ to $s$ is continuous at $\langle x, h\rangle$ in the subspace topology of $s$, where $h$ is the proof that $x \in s$.

ContinuousWithinAt.tendsto_nhdsWithin theorem

{t : Set β} (h : ContinuousWithinAt f s x) (ht : MapsTo f s t) : Tendsto f (𝓝[s] x) (𝓝[t] f x)

Full source

theorem ContinuousWithinAt.tendsto_nhdsWithin {t : Set β}
    (h : ContinuousWithinAt f s x) (ht : MapsTo f s t) :
    Tendsto f (𝓝[s] x) (𝓝[t] f x) :=
  tendsto_inf.2 ⟨h, tendsto_principal.2 <| mem_inf_of_right <| mem_principal.2 <| ht⟩

Limit Preservation Under Continuous Restriction

Informal description

Let $f : \alpha \to \beta$ be a function, $x \in \alpha$ a point, and $s \subseteq \alpha$, $t \subseteq \beta$ sets. If $f$ is continuous within $s$ at $x$ and $f$ maps $s$ into $t$, then $f$ tends to $f(x)$ in the neighborhood filter of $x$ within $s$ as a function to the neighborhood filter of $f(x)$ within $t$. In other words, the limit of $f(y)$ as $y$ approaches $x$ within $s$ exists and belongs to $t$.

ContinuousWithinAt.tendsto_nhdsWithin_image theorem

(h : ContinuousWithinAt f s x) : Tendsto f (𝓝[s] x) (𝓝[f '' s] f x)

Full source

theorem ContinuousWithinAt.tendsto_nhdsWithin_image (h : ContinuousWithinAt f s x) :
    Tendsto f (𝓝[s] x) (𝓝[f '' s] f x) :=
  h.tendsto_nhdsWithin (mapsTo_image _ _)

Limit Preservation Under Continuous Restriction to Image

Informal description

Let $f : \alpha \to \beta$ be a function between topological spaces, $s \subseteq \alpha$ a subset, and $x \in s$. If $f$ is continuous within $s$ at $x$, then $f$ tends to $f(x)$ in the neighborhood filter of $x$ within $s$ as a function to the neighborhood filter of $f(x)$ within the image $f(s)$.

nhdsWithin_le_comap theorem

(ctsf : ContinuousWithinAt f s x) : 𝓝[s] x ≤ comap f (𝓝[f '' s] f x)

Full source

theorem nhdsWithin_le_comap (ctsf : ContinuousWithinAt f s x) :
    𝓝[s] x ≤ comap f (𝓝[f '' s] f x) :=
  ctsf.tendsto_nhdsWithin_image.le_comap

Neighborhood Filter Comparison Under Continuous Restriction to Image

Informal description

Let $f : \alpha \to \beta$ be a function between topological spaces, $s \subseteq \alpha$ a subset, and $x \in s$. If $f$ is continuous within $s$ at $x$, then the neighborhood filter of $x$ within $s$ is contained in the preimage under $f$ of the neighborhood filter of $f(x)$ within the image $f(s)$. In other words, $\mathcal{N}_s(x) \leq f^{-1}(\mathcal{N}_{f(s)}(f(x)))$.

ContinuousWithinAt.preimage_mem_nhdsWithin theorem

{t : Set β} (h : ContinuousWithinAt f s x) (ht : t ∈ 𝓝 (f x)) : f ⁻¹' t ∈ 𝓝[s] x

Full source

theorem ContinuousWithinAt.preimage_mem_nhdsWithin {t : Set β}
    (h : ContinuousWithinAt f s x) (ht : t ∈ 𝓝 (f x)) : f ⁻¹' tf ⁻¹' t ∈ 𝓝[s] x :=
  h ht

Preimage of Neighborhood under Continuity within a Subset

Informal description

Let $f : \alpha \to \beta$ be a function between topological spaces, $s \subseteq \alpha$ a subset, and $x \in \alpha$. If $f$ is continuous within $s$ at $x$, then for any neighborhood $t$ of $f(x)$ in $\beta$, the preimage $f^{-1}(t)$ is a neighborhood of $x$ within $s$.

ContinuousWithinAt.preimage_mem_nhdsWithin' theorem

{t : Set β} (h : ContinuousWithinAt f s x) (ht : t ∈ 𝓝[f '' s] f x) : f ⁻¹' t ∈ 𝓝[s] x

Full source

theorem ContinuousWithinAt.preimage_mem_nhdsWithin' {t : Set β}
    (h : ContinuousWithinAt f s x) (ht : t ∈ 𝓝[f '' s] f x) : f ⁻¹' tf ⁻¹' t ∈ 𝓝[s] x :=
  h.tendsto_nhdsWithin (mapsTo_image _ _) ht

Preimage of Relative Neighborhood under Continuity within a Subset

Informal description

Let $f : \alpha \to \beta$ be a function between topological spaces, $s \subseteq \alpha$ a subset, and $x \in \alpha$. If $f$ is continuous within $s$ at $x$ and $t$ is a neighborhood of $f(x)$ within $f(s)$, then the preimage $f^{-1}(t)$ is a neighborhood of $x$ within $s$.

ContinuousWithinAt.preimage_mem_nhdsWithin'' theorem

 {y : β} {s t : Set β} (h : ContinuousWithinAt f (f ⁻¹' s) x) (ht : t ∈ 𝓝[s] y) (hxy : y = f x) : f ⁻¹' t ∈ 𝓝[f ⁻¹' s] x

Full source

theorem ContinuousWithinAt.preimage_mem_nhdsWithin'' {y : β} {s t : Set β}
    (h : ContinuousWithinAt f (f ⁻¹' s) x) (ht : t ∈ 𝓝[s] y) (hxy : y = f x) :
    f ⁻¹' tf ⁻¹' t ∈ 𝓝[f ⁻¹' s] x := by
  rw [hxy] at ht
  exact h.preimage_mem_nhdsWithin' (nhdsWithin_mono _ (image_preimage_subset f s) ht)

Preimage of Relative Neighborhood under Continuity within Preimage Set

Informal description

Let $f : \alpha \to \beta$ be a function between topological spaces, $s, t \subseteq \beta$ subsets, $x \in \alpha$, and $y \in \beta$ such that $y = f(x)$. If $f$ is continuous within $f^{-1}(s)$ at $x$ and $t$ is a neighborhood of $y$ within $s$, then the preimage $f^{-1}(t)$ is a neighborhood of $x$ within $f^{-1}(s)$.

continuousWithinAt_of_not_mem_closure theorem

(hx : x ∉ closure s) : ContinuousWithinAt f s x

Full source

theorem continuousWithinAt_of_not_mem_closure (hx : x ∉ closure s) :
    ContinuousWithinAt f s x := by
  rw [mem_closure_iff_nhdsWithin_neBot, not_neBot] at hx
  rw [ContinuousWithinAt, hx]
  exact tendsto_bot

Continuity Within a Set at Points Outside Its Closure

Informal description

For a function $f$ and a set $s$, if a point $x$ does not belong to the closure of $s$, then $f$ is continuous within $s$ at $x$.

continuousOn_iff theorem

 : ContinuousOn f s ↔ ∀ x ∈ s, ∀ t : Set β, IsOpen t → f x ∈ t → ∃ u, IsOpen u ∧ x ∈ u ∧ u ∩ s ⊆ f ⁻¹' t

Full source

theorem continuousOn_iff :
    ContinuousOnContinuousOn f s ↔
      ∀ x ∈ s, ∀ t : Set β, IsOpen t → f x ∈ t → ∃ u, IsOpen u ∧ x ∈ u ∧ u ∩ s ⊆ f ⁻¹' t := by
  simp only [ContinuousOn, ContinuousWithinAt, tendsto_nhds, mem_nhdsWithin]

Characterization of Continuity on a Set via Open Neighborhoods

Informal description

A function $f$ is continuous on a set $s$ if and only if for every point $x \in s$ and every open set $t$ containing $f(x)$, there exists an open neighborhood $u$ of $x$ such that $u \cap s$ is contained in the preimage $f^{-1}(t)$.

ContinuousOn.continuousWithinAt theorem

(hf : ContinuousOn f s) (hx : x ∈ s) : ContinuousWithinAt f s x

Full source

theorem ContinuousOn.continuousWithinAt (hf : ContinuousOn f s) (hx : x ∈ s) :
    ContinuousWithinAt f s x :=
  hf x hx

Continuity on a subset implies continuity within the subset at each point

Informal description

Let $f : \alpha \to \beta$ be a function between topological spaces, and let $s \subseteq \alpha$ be a subset. If $f$ is continuous on $s$ and $x \in s$, then $f$ is continuous at $x$ within $s$.

continuousOn_iff_continuous_restrict theorem

: ContinuousOn f s ↔ Continuous (s.restrict f)

Full source

theorem continuousOn_iff_continuous_restrict :
    ContinuousOnContinuousOn f s ↔ Continuous (s.restrict f) := by
  rw [ContinuousOn, continuous_iff_continuousAt]; constructor
  · rintro h ⟨x, xs⟩
    exact (continuousWithinAt_iff_continuousAt_restrict f xs).mp (h x xs)
  intro h x xs
  exact (continuousWithinAt_iff_continuousAt_restrict f xs).mpr (h ⟨x, xs⟩)

Characterization of Continuity on Subset via Restriction

Informal description

A function $f : \alpha \to \beta$ between topological spaces is continuous on a subset $s \subseteq \alpha$ if and only if its restriction $f|_s : s \to \beta$ is continuous when $s$ is equipped with the subspace topology.

ContinuousOn.restrict_mapsTo theorem

{t : Set β} (hf : ContinuousOn f s) (ht : MapsTo f s t) : Continuous (ht.restrict f s t)

Full source

theorem ContinuousOn.restrict_mapsTo {t : Set β} (hf : ContinuousOn f s) (ht : MapsTo f s t) :
    Continuous (ht.restrict f s t) :=
  hf.restrict.codRestrict _

Continuity of Restricted Function on Mapped Subset

Informal description

Let $f : \alpha \to \beta$ be a function between topological spaces, and let $s \subseteq \alpha$ and $t \subseteq \beta$ be subsets. If $f$ is continuous on $s$ and $f$ maps $s$ into $t$, then the restriction of $f$ to $s$ with codomain $t$ is continuous (where $t$ is equipped with the subspace topology).

continuousOn_iff' theorem

: ContinuousOn f s ↔ ∀ t : Set β, IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s

Full source

theorem continuousOn_iff' :
    ContinuousOnContinuousOn f s ↔ ∀ t : Set β, IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s := by
  have : ∀ t, IsOpenIsOpen (s.restrict f ⁻¹' t) ↔ ∃ u : Set α, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s := by
    intro t
    rw [isOpen_induced_iff, Set.restrict_eq, Set.preimage_comp]
    simp only [Subtype.preimage_coe_eq_preimage_coe_iff]
    constructor <;>
      · rintro ⟨u, ou, useq⟩
        exact ⟨u, ou, by simpa only [Set.inter_comm, eq_comm] using useq⟩
  rw [continuousOn_iff_continuous_restrict, continuous_def]; simp only [this]

Characterization of Continuity on Subset via Local Open Sets

Informal description

Let $X$ and $Y$ be topological spaces, $f : X \to Y$ a function, and $s \subseteq X$ a subset. Then $f$ is continuous on $s$ if and only if for every open set $t \subseteq Y$, there exists an open set $u \subseteq X$ such that $f^{-1}(t) \cap s = u \cap s$.

ContinuousOn.mono_dom theorem

 {α β : Type*} {t₁ t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β} (h₁ : t₂ ≤ t₁) {s : Set α} {f : α → β}
  (h₂ : @ContinuousOn α β t₁ t₃ f s) : @ContinuousOn α β t₂ t₃ f s

Full source

/-- If a function is continuous on a set for some topologies, then it is
continuous on the same set with respect to any finer topology on the source space. -/
theorem ContinuousOn.mono_dom {α β : Type*} {t₁ t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β}
    (h₁ : t₂ ≤ t₁) {s : Set α} {f : α → β} (h₂ : @ContinuousOn α β t₁ t₃ f s) :
    @ContinuousOn α β t₂ t₃ f s := fun x hx _u hu =>
  map_mono (inf_le_inf_right _ <| nhds_mono h₁) (h₂ x hx hu)

Continuity on a Set is Preserved Under Finer Topologies on the Domain

Informal description

Let $α$ and $β$ be types equipped with topological spaces $t₁$ and $t₂$ on $α$ and $t₃$ on $β$, such that $t₂$ is finer than $t₁$ (i.e., $t₂ ≤ t₁$). For any subset $s ⊆ α$ and function $f : α → β$, if $f$ is continuous on $s$ with respect to $t₁$ and $t₃$, then $f$ is also continuous on $s$ with respect to $t₂$ and $t₃$.

ContinuousOn.mono_rng theorem

 {α β : Type*} {t₁ : TopologicalSpace α} {t₂ t₃ : TopologicalSpace β} (h₁ : t₂ ≤ t₃) {s : Set α} {f : α → β}
  (h₂ : @ContinuousOn α β t₁ t₂ f s) : @ContinuousOn α β t₁ t₃ f s

Full source

/-- If a function is continuous on a set for some topologies, then it is
continuous on the same set with respect to any coarser topology on the target space. -/
theorem ContinuousOn.mono_rng {α β : Type*} {t₁ : TopologicalSpace α} {t₂ t₃ : TopologicalSpace β}
    (h₁ : t₂ ≤ t₃) {s : Set α} {f : α → β} (h₂ : @ContinuousOn α β t₁ t₂ f s) :
    @ContinuousOn α β t₁ t₃ f s := fun x hx _u hu =>
  h₂ x hx <| nhds_mono h₁ hu

Continuity on a Set is Preserved Under Coarser Topologies on the Codomain

Informal description

Let $α$ and $β$ be types equipped with topological spaces $t₁$ on $α$ and $t₂, t₃$ on $β$ such that $t₂$ is coarser than $t₃$ (i.e., $t₂ ≤ t₃$). For any subset $s ⊆ α$ and function $f : α → β$, if $f$ is continuous on $s$ with respect to $t₁$ and $t₂$, then $f$ is also continuous on $s$ with respect to $t₁$ and $t₃$.

continuousOn_iff_isClosed theorem

: ContinuousOn f s ↔ ∀ t : Set β, IsClosed t → ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s

Full source

theorem continuousOn_iff_isClosed :
    ContinuousOnContinuousOn f s ↔ ∀ t : Set β, IsClosed t → ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s := by
  have : ∀ t, IsClosedIsClosed (s.restrict f ⁻¹' t) ↔ ∃ u : Set α, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s := by
    intro t
    rw [isClosed_induced_iff, Set.restrict_eq, Set.preimage_comp]
    simp only [Subtype.preimage_coe_eq_preimage_coe_iff, eq_comm, Set.inter_comm s]
  rw [continuousOn_iff_continuous_restrict, continuous_iff_isClosed]; simp only [this]

Characterization of Continuity on Subset via Closed Sets

Informal description

Let $X$ and $Y$ be topological spaces, $f : X \to Y$ a function, and $s \subseteq X$ a subset. Then $f$ is continuous on $s$ if and only if for every closed set $t \subseteq Y$, there exists a closed set $u \subseteq X$ such that $f^{-1}(t) \cap s = u \cap s$.

continuous_of_cover_nhds theorem

 {ι : Sort*} {s : ι → Set α} (hs : ∀ x : α, ∃ i, s i ∈ 𝓝 x) (hf : ∀ i, ContinuousOn f (s i)) : Continuous f

Full source

theorem continuous_of_cover_nhds {ι : Sort*} {s : ι → Set α}
    (hs : ∀ x : α, ∃ i, s i ∈ 𝓝 x) (hf : ∀ i, ContinuousOn f (s i)) :
    Continuous f :=
  continuous_iff_continuousAt.mpr fun x ↦ let ⟨i, hi⟩ := hs x; by
    rw [ContinuousAt, ← nhdsWithin_eq_nhds.2 hi]
    exact hf _ _ (mem_of_mem_nhds hi)

Global Continuity via Local Continuity on a Cover by Neighborhoods

Informal description

Let $X$ and $Y$ be topological spaces, $f : X \to Y$ a function, and $\{s_i\}_{i \in I}$ a family of subsets of $X$ such that for every $x \in X$, there exists $i \in I$ with $s_i$ being a neighborhood of $x$. If $f$ is continuous on each $s_i$, then $f$ is continuous on $X$.

continuousOn_empty theorem

(f : α → β) : ContinuousOn f ∅

Full source

@[simp] theorem continuousOn_empty (f : α → β) : ContinuousOn f ∅ := fun _ => False.elim

Continuity on the Empty Set

Informal description

For any function $f : \alpha \to \beta$, $f$ is continuous on the empty set $\emptyset$.

continuousOn_singleton theorem

(f : α → β) (a : α) : ContinuousOn f { a }

Full source

@[simp]
theorem continuousOn_singleton (f : α → β) (a : α) : ContinuousOn f {a} :=
  forall_eq.2 <| by
    simpa only [ContinuousWithinAt, nhdsWithin_singleton, tendsto_pure_left] using fun s =>
      mem_of_mem_nhds

Continuity on a Singleton Set

Informal description

For any function $f : \alpha \to \beta$ between topological spaces and any point $a \in \alpha$, the function $f$ is continuous on the singleton set $\{a\}$.

Set.Subsingleton.continuousOn theorem

{s : Set α} (hs : s.Subsingleton) (f : α → β) : ContinuousOn f s

Full source

theorem Set.Subsingleton.continuousOn {s : Set α} (hs : s.Subsingleton) (f : α → β) :
    ContinuousOn f s :=
  hs.induction_on (continuousOn_empty f) (continuousOn_singleton f)

Continuity on Subsingleton Sets

Informal description

For any subset $s$ of a topological space $\alpha$ that is a subsingleton (i.e., contains at most one element), and any function $f : \alpha \to \beta$ to another topological space $\beta$, the function $f$ is continuous on $s$.

continuousOn_open_iff theorem

(hs : IsOpen s) : ContinuousOn f s ↔ ∀ t, IsOpen t → IsOpen (s ∩ f ⁻¹' t)

Full source

theorem continuousOn_open_iff (hs : IsOpen s) :
    ContinuousOnContinuousOn f s ↔ ∀ t, IsOpen t → IsOpen (s ∩ f ⁻¹' t) := by
  rw [continuousOn_iff']
  constructor
  · intro h t ht
    rcases h t ht with ⟨u, u_open, hu⟩
    rw [inter_comm, hu]
    apply IsOpen.inter u_open hs
  · intro h t ht
    refine ⟨s ∩ f ⁻¹' t, h t ht, ?_⟩
    rw [@inter_comm _ s (f ⁻¹' t), inter_assoc, inter_self]

Characterization of Continuity on Open Subset via Preimages of Open Sets

Informal description

Let $X$ and $Y$ be topological spaces, $f : X \to Y$ a function, and $s \subseteq X$ an open subset. Then $f$ is continuous on $s$ if and only if for every open set $t \subseteq Y$, the intersection $s \cap f^{-1}(t)$ is open in $X$.

ContinuousOn.isOpen_inter_preimage theorem

{t : Set β} (hf : ContinuousOn f s) (hs : IsOpen s) (ht : IsOpen t) : IsOpen (s ∩ f ⁻¹' t)

Full source

theorem ContinuousOn.isOpen_inter_preimage {t : Set β}
    (hf : ContinuousOn f s) (hs : IsOpen s) (ht : IsOpen t) : IsOpen (s ∩ f ⁻¹' t) :=
  (continuousOn_open_iff hs).1 hf t ht

Openness of Intersection with Preimage under Continuous Function on Open Domain

Informal description

Let $X$ and $Y$ be topological spaces, $f : X \to Y$ a function, and $s \subseteq X$ an open subset. If $f$ is continuous on $s$ and $t \subseteq Y$ is open, then the intersection $s \cap f^{-1}(t)$ is open in $X$.

ContinuousOn.isOpen_preimage theorem

{t : Set β} (h : ContinuousOn f s) (hs : IsOpen s) (hp : f ⁻¹' t ⊆ s) (ht : IsOpen t) : IsOpen (f ⁻¹' t)

Full source

theorem ContinuousOn.isOpen_preimage {t : Set β} (h : ContinuousOn f s)
    (hs : IsOpen s) (hp : f ⁻¹' tf ⁻¹' t ⊆ s) (ht : IsOpen t) : IsOpen (f ⁻¹' t) := by
  convert (continuousOn_open_iff hs).mp h t ht
  rw [inter_comm, inter_eq_self_of_subset_left hp]

Openness of Preimage under Continuous Function on Open Domain

Informal description

Let $X$ and $Y$ be topological spaces, $f : X \to Y$ a function, and $s \subseteq X$ an open subset. If $f$ is continuous on $s$, the preimage $f^{-1}(t) \subseteq s$ for some open set $t \subseteq Y$, then $f^{-1}(t)$ is open in $X$.

ContinuousOn.preimage_isClosed_of_isClosed theorem

{t : Set β} (hf : ContinuousOn f s) (hs : IsClosed s) (ht : IsClosed t) : IsClosed (s ∩ f ⁻¹' t)

Full source

theorem ContinuousOn.preimage_isClosed_of_isClosed {t : Set β}
    (hf : ContinuousOn f s) (hs : IsClosed s) (ht : IsClosed t) : IsClosed (s ∩ f ⁻¹' t) := by
  rcases continuousOn_iff_isClosed.1 hf t ht with ⟨u, hu⟩
  rw [inter_comm, hu.2]
  apply IsClosed.inter hu.1 hs

Preimage of Closed Set under Continuous Function on Closed Domain is Closed

Informal description

Let $X$ and $Y$ be topological spaces, $f : X \to Y$ a function, and $s \subseteq X$ a closed subset. If $f$ is continuous on $s$ and $t \subseteq Y$ is closed, then the intersection $s \cap f^{-1}(t)$ is closed in $X$.

ContinuousOn.preimage_interior_subset_interior_preimage theorem

{t : Set β} (hf : ContinuousOn f s) (hs : IsOpen s) : s ∩ f ⁻¹' interior t ⊆ s ∩ interior (f ⁻¹' t)

Full source

theorem ContinuousOn.preimage_interior_subset_interior_preimage {t : Set β}
    (hf : ContinuousOn f s) (hs : IsOpen s) : s ∩ f ⁻¹' interior ts ∩ f ⁻¹' interior t ⊆ s ∩ interior (f ⁻¹' t) :=
  calc
    s ∩ f ⁻¹' interior ts ∩ f ⁻¹' interior t ⊆ interior (s ∩ f ⁻¹' t) :=
      interior_maximal (inter_subset_inter (Subset.refl _) (preimage_mono interior_subset))
        (hf.isOpen_inter_preimage hs isOpen_interior)
    _ = s ∩ interior (f ⁻¹' t) := by rw [interior_inter, hs.interior_eq]

Inclusion of Preimage of Interior under Continuous Function on Open Domain

Informal description

Let $X$ and $Y$ be topological spaces, $f : X \to Y$ a function, and $s \subseteq X$ an open subset. If $f$ is continuous on $s$, then for any subset $t \subseteq Y$, the intersection of $s$ with the preimage of the interior of $t$ is contained in the intersection of $s$ with the interior of the preimage of $t$. In other words: $$ s \cap f^{-1}(\text{int } t) \subseteq s \cap \text{int}(f^{-1}(t)) $$

continuousOn_of_locally_continuousOn theorem

(h : ∀ x ∈ s, ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)) : ContinuousOn f s

Full source

theorem continuousOn_of_locally_continuousOn
    (h : ∀ x ∈ s, ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)) : ContinuousOn f s := by
  intro x xs
  rcases h x xs with ⟨t, open_t, xt, ct⟩
  have := ct x ⟨xs, xt⟩
  rwa [ContinuousWithinAt, ← nhdsWithin_restrict _ xt open_t] at this

Local Continuity Implies Global Continuity on a Set

Informal description

Let $f : \alpha \to \beta$ be a function between topological spaces and $s \subseteq \alpha$ a subset. If for every point $x \in s$ there exists an open neighborhood $t$ of $x$ such that $f$ is continuous on $s \cap t$, then $f$ is continuous on $s$.

continuousOn_to_generateFrom_iff theorem

 {β : Type*} {T : Set (Set β)} {f : α → β} :
  @ContinuousOn α β _ (.generateFrom T) f s ↔ ∀ x ∈ s, ∀ t ∈ T, f x ∈ t → f ⁻¹' t ∈ 𝓝[s] x

Full source

theorem continuousOn_to_generateFrom_iff {β : Type*} {T : Set (Set β)} {f : α → β} :
    @ContinuousOn α β _ (.generateFrom T) f s ↔ ∀ x ∈ s, ∀ t ∈ T, f x ∈ t → f ⁻¹' t ∈ 𝓝[s] x :=
  forall₂_congr fun x _ => by
    delta ContinuousWithinAt
    simp only [TopologicalSpace.nhds_generateFrom, tendsto_iInf, tendsto_principal, mem_setOf_eq,
      and_imp]
    exact forall_congr' fun t => forall_swap

Characterization of Continuity on a Set via Subbasis

Informal description

Let $T$ be a collection of subsets of a topological space $\beta$, and let $f : \alpha \to \beta$ be a function defined on a subset $s \subseteq \alpha$. Then $f$ is continuous on $s$ with respect to the topology generated by $T$ if and only if for every $x \in s$ and every $t \in T$ containing $f(x)$, the preimage $f^{-1}(t)$ is a neighborhood of $x$ within $s$.

continuousOn_isOpen_of_generateFrom theorem

 {β : Type*} {s : Set α} {T : Set (Set β)} {f : α → β} (h : ∀ t ∈ T, IsOpen (s ∩ f ⁻¹' t)) :
  @ContinuousOn α β _ (.generateFrom T) f s

Full source

theorem continuousOn_isOpen_of_generateFrom {β : Type*} {s : Set α} {T : Set (Set β)} {f : α → β}
    (h : ∀ t ∈ T, IsOpen (s ∩ f ⁻¹' t)) :
    @ContinuousOn α β _ (.generateFrom T) f s :=
  continuousOn_to_generateFrom_iff.2 fun _x hx t ht hxt => mem_nhdsWithin.2
    ⟨_, h t ht, ⟨hx, hxt⟩, fun _y hy => hy.1.2⟩

Open Preimage Condition Implies Continuity with Respect to Generated Topology

Informal description

Let $\alpha$ and $\beta$ be topological spaces, $s \subseteq \alpha$ a subset, $T$ a collection of subsets of $\beta$, and $f : \alpha \to \beta$ a function. If for every $t \in T$, the set $s \cap f^{-1}(t)$ is open in $\alpha$, then $f$ is continuous on $s$ with respect to the topology on $\beta$ generated by $T$.

ContinuousWithinAt.mono theorem

(h : ContinuousWithinAt f t x) (hs : s ⊆ t) : ContinuousWithinAt f s x

Full source

theorem ContinuousWithinAt.mono (h : ContinuousWithinAt f t x)
    (hs : s ⊆ t) : ContinuousWithinAt f s x :=
  h.mono_left (nhdsWithin_mono x hs)

Restriction Preserves Continuity Within a Set

Informal description

Let $f : \alpha \to \beta$ be a function between topological spaces, and let $x \in s \subseteq t \subseteq \alpha$. If $f$ is continuous within $t$ at $x$, then $f$ is also continuous within $s$ at $x$.

ContinuousWithinAt.mono_of_mem_nhdsWithin theorem

(h : ContinuousWithinAt f t x) (hs : t ∈ 𝓝[s] x) : ContinuousWithinAt f s x

Full source

theorem ContinuousWithinAt.mono_of_mem_nhdsWithin (h : ContinuousWithinAt f t x) (hs : t ∈ 𝓝[s] x) :
    ContinuousWithinAt f s x :=
  h.mono_left (nhdsWithin_le_of_mem hs)

Continuity Within a Set via Neighborhood Inclusion

Informal description

Let $f : \alpha \to \beta$ be a function between topological spaces, and let $x \in s \subseteq \alpha$. If $f$ is continuous within a set $t \subseteq \alpha$ at $x$, and $t$ is a neighborhood of $x$ within $s$, then $f$ is also continuous within $s$ at $x$.

continuousWithinAt_congr_set theorem

(h : s =ᶠ[𝓝 x] t) : ContinuousWithinAt f s x ↔ ContinuousWithinAt f t x

Full source

/-- If two sets coincide around `x`, then being continuous within one or the other at `x` is
equivalent. See also `continuousWithinAt_congr_set'` which requires that the sets coincide
locally away from a point `y`, in a T1 space. -/
theorem continuousWithinAt_congr_set (h : s =ᶠ[𝓝 x] t) :
    ContinuousWithinAtContinuousWithinAt f s x ↔ ContinuousWithinAt f t x := by
  simp only [ContinuousWithinAt, nhdsWithin_eq_iff_eventuallyEq.mpr h]

Equivalence of Continuity Within Sets That Coincide Near a Point

Informal description

Let $f : \alpha \to \beta$ be a function between topological spaces, and let $x \in \alpha$. If two sets $s, t \subseteq \alpha$ are eventually equal in the neighborhood filter of $x$ (i.e., $s =_{\mathcal{N}(x)} t$), then $f$ is continuous within $s$ at $x$ if and only if $f$ is continuous within $t$ at $x$.

ContinuousWithinAt.congr_set theorem

(hf : ContinuousWithinAt f s x) (h : s =ᶠ[𝓝 x] t) : ContinuousWithinAt f t x

Full source

theorem ContinuousWithinAt.congr_set (hf : ContinuousWithinAt f s x) (h : s =ᶠ[𝓝 x] t) :
    ContinuousWithinAt f t x :=
  (continuousWithinAt_congr_set h).1 hf

Continuity Within Set is Preserved Under Local Set Equality

Informal description

Let $f : \alpha \to \beta$ be a function between topological spaces, and let $x \in \alpha$. If $f$ is continuous within a set $s \subseteq \alpha$ at $x$, and $s$ is eventually equal to another set $t \subseteq \alpha$ in the neighborhood filter of $x$ (i.e., $s =_{\mathcal{N}(x)} t$), then $f$ is also continuous within $t$ at $x$.

continuousWithinAt_inter' theorem

(h : t ∈ 𝓝[s] x) : ContinuousWithinAt f (s ∩ t) x ↔ ContinuousWithinAt f s x

Full source

theorem continuousWithinAt_inter' (h : t ∈ 𝓝[s] x) :
    ContinuousWithinAtContinuousWithinAt f (s ∩ t) x ↔ ContinuousWithinAt f s x := by
  simp [ContinuousWithinAt, nhdsWithin_restrict'' s h]

Continuity Within Intersection of Neighborhood is Equivalent to Continuity Within Original Set

Informal description

For a function $f : \alpha \to \beta$ between topological spaces, a point $x \in \alpha$, and sets $s, t \subseteq \alpha$, if $t$ is a neighborhood of $x$ within $s$ (i.e., $t \in \mathcal{N}_s(x)$), then $f$ is continuous at $x$ within $s \cap t$ if and only if $f$ is continuous at $x$ within $s$.

continuousWithinAt_inter theorem

(h : t ∈ 𝓝 x) : ContinuousWithinAt f (s ∩ t) x ↔ ContinuousWithinAt f s x

Full source

theorem continuousWithinAt_inter (h : t ∈ 𝓝 x) :
    ContinuousWithinAtContinuousWithinAt f (s ∩ t) x ↔ ContinuousWithinAt f s x := by
  simp [ContinuousWithinAt, nhdsWithin_restrict' s h]

Continuity Within Intersection of Neighborhood is Equivalent to Continuity Within Original Set

Informal description

For a function $f : \alpha \to \beta$ between topological spaces, a point $x \in \alpha$, and sets $s, t \subseteq \alpha$, if $t$ is a neighborhood of $x$ (i.e., $t \in \mathcal{N}(x)$), then $f$ is continuous at $x$ within $s \cap t$ if and only if $f$ is continuous at $x$ within $s$.

continuousWithinAt_union theorem

: ContinuousWithinAt f (s ∪ t) x ↔ ContinuousWithinAt f s x ∧ ContinuousWithinAt f t x

Full source

theorem continuousWithinAt_union :
    ContinuousWithinAtContinuousWithinAt f (s ∪ t) x ↔ ContinuousWithinAt f s x ∧ ContinuousWithinAt f t x := by
  simp only [ContinuousWithinAt, nhdsWithin_union, tendsto_sup]

Continuity Within Union is Equivalent to Continuity Within Each Set

Informal description

A function $f$ is continuous at a point $x$ within the union of two sets $s$ and $t$ if and only if it is continuous at $x$ within $s$ and within $t$ separately. In other words, \[ f \text{ is continuous at } x \text{ within } s \cup t \leftrightarrow f \text{ is continuous at } x \text{ within } s \land f \text{ is continuous at } x \text{ within } t. \]

ContinuousWithinAt.union theorem

(hs : ContinuousWithinAt f s x) (ht : ContinuousWithinAt f t x) : ContinuousWithinAt f (s ∪ t) x

Full source

theorem ContinuousWithinAt.union (hs : ContinuousWithinAt f s x) (ht : ContinuousWithinAt f t x) :
    ContinuousWithinAt f (s ∪ t) x :=
  continuousWithinAt_union.2 ⟨hs, ht⟩

Continuity Within Union of Sets

Informal description

If a function $f$ is continuous at a point $x$ within sets $s$ and $t$, then it is also continuous at $x$ within their union $s \cup t$.

continuousWithinAt_singleton theorem

: ContinuousWithinAt f { x } x

Full source

@[simp]
theorem continuousWithinAt_singleton : ContinuousWithinAt f {x} x := by
  simp only [ContinuousWithinAt, nhdsWithin_singleton, tendsto_pure_nhds]

Continuity Within Singleton Set at the Point

Informal description

For any function $f$ between topological spaces and any point $x$, the function $f$ is continuous at $x$ within the singleton set $\{x\}$.

continuousWithinAt_insert_self theorem

: ContinuousWithinAt f (insert x s) x ↔ ContinuousWithinAt f s x

Full source

@[simp]
theorem continuousWithinAt_insert_self :
    ContinuousWithinAtContinuousWithinAt f (insert x s) x ↔ ContinuousWithinAt f s x := by
  simp only [← singleton_union, continuousWithinAt_union, continuousWithinAt_singleton, true_and]

Continuity at a point within a set with inserted point

Informal description

A function $f$ is continuous at a point $x$ within the set $\{x\} \cup s$ if and only if it is continuous at $x$ within the set $s$.

ContinuousWithinAt.diff_iff theorem

(ht : ContinuousWithinAt f t x) : ContinuousWithinAt f (s \ t) x ↔ ContinuousWithinAt f s x

Full source

theorem ContinuousWithinAt.diff_iff
    (ht : ContinuousWithinAt f t x) : ContinuousWithinAtContinuousWithinAt f (s \ t) x ↔ ContinuousWithinAt f s x :=
  ⟨fun h => (h.union ht).mono <| by simp only [diff_union_self, subset_union_left], fun h =>
    h.mono diff_subset⟩

Continuity Within Set Difference vs Original Set

Informal description

Let $f : \alpha \to \beta$ be a function between topological spaces, $x \in s \subseteq \alpha$, and suppose $f$ is continuous within $t$ at $x$. Then $f$ is continuous within $s \setminus t$ at $x$ if and only if $f$ is continuous within $s$ at $x$.

continuousWithinAt_diff_self theorem

: ContinuousWithinAt f (s \ { x }) x ↔ ContinuousWithinAt f s x

Full source

/-- See also `continuousWithinAt_diff_singleton` for the case of `s \ {y}`, but
requiring `T1Space α. -/
@[simp]
theorem continuousWithinAt_diff_self :
    ContinuousWithinAtContinuousWithinAt f (s \ {x}) x ↔ ContinuousWithinAt f s x :=
  continuousWithinAt_singleton.diff_iff

Continuity at a point within a set minus the point vs within the original set

Informal description

For a function $f : \alpha \to \beta$ between topological spaces and a point $x \in s \subseteq \alpha$, the function $f$ is continuous at $x$ within the set $s \setminus \{x\}$ if and only if $f$ is continuous at $x$ within the set $s$.

continuousWithinAt_compl_self theorem

: ContinuousWithinAt f { x }ᶜ x ↔ ContinuousAt f x

Full source

@[simp]
theorem continuousWithinAt_compl_self :
    ContinuousWithinAtContinuousWithinAt f {x}ᶜ x ↔ ContinuousAt f x := by
  rw [compl_eq_univ_diff, continuousWithinAt_diff_self, continuousWithinAt_univ]

Continuity at a point vs continuity within the complement of the point

Informal description

For a function $f \colon \alpha \to \beta$ between topological spaces and a point $x \in \alpha$, the function $f$ is continuous at $x$ within the complement of $\{x\}$ if and only if $f$ is continuous at $x$.

ContinuousOn.mono theorem

(hf : ContinuousOn f s) (h : t ⊆ s) : ContinuousOn f t

Full source

theorem ContinuousOn.mono (hf : ContinuousOn f s) (h : t ⊆ s) :
    ContinuousOn f t := fun x hx => (hf x (h hx)).mono_left (nhdsWithin_mono _ h)

Continuity on Subset: Restriction Preserves Continuity

Informal description

Let $f : \alpha \to \beta$ be a function, and let $s, t$ be subsets of $\alpha$ with $t \subseteq s$. If $f$ is continuous on $s$, then $f$ is continuous on $t$.

antitone_continuousOn theorem

{f : α → β} : Antitone (ContinuousOn f)

Full source

theorem antitone_continuousOn {f : α → β} : Antitone (ContinuousOn f) := fun _s _t hst hf =>
  hf.mono hst

Antitonicity of Continuity on Subsets

Informal description

For any function $f : \alpha \to \beta$, the function that maps a subset $s \subseteq \alpha$ to the proposition "$f$ is continuous on $s$" is antitone. That is, if $t \subseteq s \subseteq \alpha$, then continuity of $f$ on $s$ implies continuity of $f$ on $t$.

ContinuousAt.continuousWithinAt theorem

(h : ContinuousAt f x) : ContinuousWithinAt f s x

Full source

theorem ContinuousAt.continuousWithinAt (h : ContinuousAt f x) :
    ContinuousWithinAt f s x :=
  ContinuousWithinAt.mono ((continuousWithinAt_univ f x).2 h) (subset_univ _)

Pointwise Continuity Implies Continuity Within Any Subset

Informal description

For any function $f \colon \alpha \to \beta$ between topological spaces and any point $x \in \alpha$, if $f$ is continuous at $x$, then $f$ is continuous within any subset $s \subseteq \alpha$ at $x$.

continuousWithinAt_iff_continuousAt theorem

(h : s ∈ 𝓝 x) : ContinuousWithinAt f s x ↔ ContinuousAt f x

Full source

theorem continuousWithinAt_iff_continuousAt (h : s ∈ 𝓝 x) :
    ContinuousWithinAtContinuousWithinAt f s x ↔ ContinuousAt f x := by
  rw [← univ_inter s, continuousWithinAt_inter h, continuousWithinAt_univ]

Equivalence of Continuity Within a Neighborhood and Pointwise Continuity

Informal description

For a function $f \colon \alpha \to \beta$ between topological spaces, a point $x \in \alpha$, and a set $s \subseteq \alpha$, if $s$ is a neighborhood of $x$ (i.e., $s \in \mathcal{N}(x)$), then $f$ is continuous at $x$ within $s$ if and only if $f$ is continuous at $x$.

ContinuousWithinAt.continuousAt theorem

(h : ContinuousWithinAt f s x) (hs : s ∈ 𝓝 x) : ContinuousAt f x

Full source

theorem ContinuousWithinAt.continuousAt
    (h : ContinuousWithinAt f s x) (hs : s ∈ 𝓝 x) : ContinuousAt f x :=
  (continuousWithinAt_iff_continuousAt hs).mp h

Continuity Within a Neighborhood Implies Pointwise Continuity

Informal description

For a function $f \colon \alpha \to \beta$ between topological spaces, a point $x \in \alpha$, and a set $s \subseteq \alpha$, if $f$ is continuous at $x$ within $s$ and $s$ is a neighborhood of $x$ (i.e., $s \in \mathcal{N}(x)$), then $f$ is continuous at $x$.

IsOpen.continuousOn_iff theorem

(hs : IsOpen s) : ContinuousOn f s ↔ ∀ ⦃a⦄, a ∈ s → ContinuousAt f a

Full source

theorem IsOpen.continuousOn_iff (hs : IsOpen s) :
    ContinuousOnContinuousOn f s ↔ ∀ ⦃a⦄, a ∈ s → ContinuousAt f a :=
  forall₂_congr fun _ => continuousWithinAt_iff_continuousAtcontinuousWithinAt_iff_continuousAt ∘ hs.mem_nhds

Characterization of Continuity on Open Sets via Pointwise Continuity

Informal description

For an open set $s$ in a topological space and a function $f$ from this space to another topological space, $f$ is continuous on $s$ if and only if $f$ is continuous at every point $a \in s$.

ContinuousOn.continuousAt theorem

(h : ContinuousOn f s) (hx : s ∈ 𝓝 x) : ContinuousAt f x

Full source

theorem ContinuousOn.continuousAt (h : ContinuousOn f s)
    (hx : s ∈ 𝓝 x) : ContinuousAt f x :=
  (h x (mem_of_mem_nhds hx)).continuousAt hx

Continuity on a Neighborhood Implies Pointwise Continuity

Informal description

For a function $f \colon \alpha \to \beta$ between topological spaces, a point $x \in \alpha$, and a set $s \subseteq \alpha$, if $f$ is continuous on $s$ and $s$ is a neighborhood of $x$ (i.e., $s \in \mathcal{N}(x)$), then $f$ is continuous at $x$.

continuousOn_of_forall_continuousAt theorem

(hcont : ∀ x ∈ s, ContinuousAt f x) : ContinuousOn f s

Full source

theorem continuousOn_of_forall_continuousAt (hcont : ∀ x ∈ s, ContinuousAt f x) :
    ContinuousOn f s := fun x hx => (hcont x hx).continuousWithinAt

Continuity on a Set via Pointwise Continuity

Informal description

For any function $f \colon \alpha \to \beta$ between topological spaces and any subset $s \subseteq \alpha$, if $f$ is continuous at every point $x \in s$, then $f$ is continuous on $s$.

Continuous.continuousOn theorem

(h : Continuous f) : ContinuousOn f s

Full source

@[fun_prop]
theorem Continuous.continuousOn (h : Continuous f) : ContinuousOn f s := by
  rw [continuous_iff_continuousOn_univ] at h
  exact h.mono (subset_univ _)

Global Continuity Implies Continuity on Subsets

Informal description

If a function $f \colon \alpha \to \beta$ is continuous, then it is continuous on any subset $s \subseteq \alpha$.

Continuous.continuousWithinAt theorem

(h : Continuous f) : ContinuousWithinAt f s x

Full source

theorem Continuous.continuousWithinAt (h : Continuous f) :
    ContinuousWithinAt f s x :=
  h.continuousAt.continuousWithinAt

Global Continuity Implies Continuity Within Any Subset at Any Point

Informal description

If a function $f \colon X \to Y$ between topological spaces is continuous, then for any subset $s \subseteq X$ and any point $x \in X$, $f$ is continuous within $s$ at $x$.

ContinuousOn.congr_mono theorem

(h : ContinuousOn f s) (h' : EqOn g f s₁) (h₁ : s₁ ⊆ s) : ContinuousOn g s₁

Full source

theorem ContinuousOn.congr_mono (h : ContinuousOn f s) (h' : EqOn g f s₁) (h₁ : s₁ ⊆ s) :
    ContinuousOn g s₁ := by
  intro x hx
  unfold ContinuousWithinAt
  have A := (h x (h₁ hx)).mono h₁
  unfold ContinuousWithinAt at A
  rw [← h' hx] at A
  exact A.congr' h'.eventuallyEq_nhdsWithin.symm

Continuity of Restricted Function via Agreement on Subset

Informal description

Let $f, g : \alpha \to \beta$ be functions between topological spaces, and let $s_1 \subseteq s \subseteq \alpha$ be subsets. If $f$ is continuous on $s$ and $f$ and $g$ agree on $s_1$ (i.e., $f(x) = g(x)$ for all $x \in s_1$), then $g$ is continuous on $s_1$.

ContinuousOn.congr theorem

(h : ContinuousOn f s) (h' : EqOn g f s) : ContinuousOn g s

Full source

theorem ContinuousOn.congr (h : ContinuousOn f s) (h' : EqOn g f s) :
    ContinuousOn g s :=
  h.congr_mono h' (Subset.refl _)

Continuity of Function via Agreement on Domain

Informal description

Let $f, g : \alpha \to \beta$ be functions between topological spaces, and let $s \subseteq \alpha$ be a subset. If $f$ is continuous on $s$ and $f$ and $g$ agree on $s$ (i.e., $f(x) = g(x)$ for all $x \in s$), then $g$ is continuous on $s$.

continuousOn_congr theorem

(h' : EqOn g f s) : ContinuousOn g s ↔ ContinuousOn f s

Full source

theorem continuousOn_congr (h' : EqOn g f s) :
    ContinuousOnContinuousOn g s ↔ ContinuousOn f s :=
  ⟨fun h => ContinuousOn.congr h h'.symm, fun h => h.congr h'⟩

Equivalence of Continuity for Functions Agreeing on a Subset

Informal description

Let $f, g : \alpha \to \beta$ be functions between topological spaces, and let $s \subseteq \alpha$ be a subset. If $f$ and $g$ agree on $s$ (i.e., $f(x) = g(x)$ for all $x \in s$), then $g$ is continuous on $s$ if and only if $f$ is continuous on $s$.

Filter.EventuallyEq.congr_continuousWithinAt theorem

(h : f =ᶠ[𝓝[s] x] g) (hx : f x = g x) : ContinuousWithinAt f s x ↔ ContinuousWithinAt g s x

Full source

theorem Filter.EventuallyEq.congr_continuousWithinAt (h : f =ᶠ[𝓝[s] x] g) (hx : f x = g x) :
    ContinuousWithinAtContinuousWithinAt f s x ↔ ContinuousWithinAt g s x := by
  rw [ContinuousWithinAt, hx, tendsto_congr' h, ContinuousWithinAt]

Equality of Functions in Neighborhood Filter Preserves Continuity Within Set at Point

Informal description

Let $f$ and $g$ be functions that are eventually equal in the neighborhood filter of $x$ within $s$ (denoted $f =_{𝓝[s]x} g$), and satisfy $f(x) = g(x)$. Then $f$ is continuous within $s$ at $x$ if and only if $g$ is continuous within $s$ at $x$.

ContinuousWithinAt.congr_of_eventuallyEq theorem

(h : ContinuousWithinAt f s x) (h₁ : g =ᶠ[𝓝[s] x] f) (hx : g x = f x) : ContinuousWithinAt g s x

Full source

theorem ContinuousWithinAt.congr_of_eventuallyEq
    (h : ContinuousWithinAt f s x) (h₁ : g =ᶠ[𝓝[s] x] f) (hx : g x = f x) :
    ContinuousWithinAt g s x :=
  (h₁.congr_continuousWithinAt hx).2 h

Continuity Within Set at Point Preserved by Eventual Equality

Informal description

Let $f$ be a function that is continuous within a set $s$ at a point $x$. If $g$ is a function that is eventually equal to $f$ in the neighborhood filter of $x$ within $s$ (denoted $g =_{𝓝[s]x} f$) and satisfies $g(x) = f(x)$, then $g$ is also continuous within $s$ at $x$.

ContinuousWithinAt.congr_of_eventuallyEq_of_mem theorem

(h : ContinuousWithinAt f s x) (h₁ : g =ᶠ[𝓝[s] x] f) (hx : x ∈ s) : ContinuousWithinAt g s x

Full source

theorem ContinuousWithinAt.congr_of_eventuallyEq_of_mem
    (h : ContinuousWithinAt f s x) (h₁ : g =ᶠ[𝓝[s] x] f) (hx : x ∈ s) :
    ContinuousWithinAt g s x :=
  h.congr_of_eventuallyEq h₁ (mem_of_mem_nhdsWithin hx h₁ :)

Continuity within a set at a point is preserved by eventual equality when the point is in the set

Informal description

Let $f$ be a function that is continuous within a set $s$ at a point $x$. If $g$ is a function that is eventually equal to $f$ in the neighborhood filter of $x$ within $s$ (i.e., $g$ and $f$ coincide on some neighborhood of $x$ intersected with $s$), and $x \in s$, then $g$ is also continuous within $s$ at $x$.

Filter.EventuallyEq.congr_continuousWithinAt_of_mem theorem

(h : f =ᶠ[𝓝[s] x] g) (hx : x ∈ s) : ContinuousWithinAt f s x ↔ ContinuousWithinAt g s x

Full source

theorem Filter.EventuallyEq.congr_continuousWithinAt_of_mem (h : f =ᶠ[𝓝[s] x] g) (hx : x ∈ s) :
    ContinuousWithinAtContinuousWithinAt f s x ↔ ContinuousWithinAt g s x :=
  ⟨fun h' ↦ h'.congr_of_eventuallyEq_of_mem h.symm hx,
    fun h' ↦  h'.congr_of_eventuallyEq_of_mem h hx⟩

Equivalence of Continuity Within a Set at a Point for Eventually Equal Functions

Informal description

For functions $f$ and $g$ that are eventually equal in the neighborhood filter of $x$ within a set $s$ (i.e., $f =_{\mathcal{N}_s(x)} g$), and for a point $x \in s$, the function $f$ is continuous within $s$ at $x$ if and only if $g$ is continuous within $s$ at $x$.

ContinuousWithinAt.congr_of_eventuallyEq_insert theorem

(h : ContinuousWithinAt f s x) (h₁ : g =ᶠ[𝓝[insert x s] x] f) : ContinuousWithinAt g s x

Full source

theorem ContinuousWithinAt.congr_of_eventuallyEq_insert
    (h : ContinuousWithinAt f s x) (h₁ : g =ᶠ[𝓝[insert x s] x] f) :
    ContinuousWithinAt g s x :=
  h.congr_of_eventuallyEq (nhdsWithin_mono _ (subset_insert _ _) h₁)
    (mem_of_mem_nhdsWithin (mem_insert _ _) h₁ :)

Continuity Within Set at Point Preserved by Eventual Equality on Inserted Point

Informal description

Let $f$ be a function that is continuous within a set $s$ at a point $x$. If $g$ is a function that is eventually equal to $f$ in the neighborhood filter of $x$ within the set $\{x\} \cup s$ (i.e., $g =_{\mathcal{N}_{\{x\} \cup s}(x)} f$), then $g$ is also continuous within $s$ at $x$.

Filter.EventuallyEq.congr_continuousWithinAt_of_insert theorem

(h : f =ᶠ[𝓝[insert x s] x] g) : ContinuousWithinAt f s x ↔ ContinuousWithinAt g s x

Full source

theorem Filter.EventuallyEq.congr_continuousWithinAt_of_insert (h : f =ᶠ[𝓝[insert x s] x] g) :
    ContinuousWithinAtContinuousWithinAt f s x ↔ ContinuousWithinAt g s x :=
  ⟨fun h' ↦ h'.congr_of_eventuallyEq_insert h.symm,
    fun h' ↦  h'.congr_of_eventuallyEq_insert h⟩

Equivalence of Continuity Within Set at Point Under Eventual Equality on Inserted Point

Informal description

For functions $f$ and $g$ and a set $s$, if $f$ and $g$ are eventually equal in the neighborhood filter of $x$ within the set $\{x\} \cup s$ (i.e., $f =_{\mathcal{N}_{\{x\} \cup s}(x)} g$), then $f$ is continuous within $s$ at $x$ if and only if $g$ is continuous within $s$ at $x$.

ContinuousWithinAt.congr theorem

(h : ContinuousWithinAt f s x) (h₁ : ∀ y ∈ s, g y = f y) (hx : g x = f x) : ContinuousWithinAt g s x

Full source

theorem ContinuousWithinAt.congr (h : ContinuousWithinAt f s x)
    (h₁ : ∀ y ∈ s, g y = f y) (hx : g x = f x) : ContinuousWithinAt g s x :=
  h.congr_of_eventuallyEq (mem_of_superset self_mem_nhdsWithin h₁) hx

Continuity Within Set at Point Preserved by Pointwise Equality

Informal description

Let $f$ be a function that is continuous within a set $s$ at a point $x$. If $g$ is a function such that $g(y) = f(y)$ for all $y \in s$ and $g(x) = f(x)$, then $g$ is also continuous within $s$ at $x$.

continuousWithinAt_congr theorem

(h₁ : ∀ y ∈ s, g y = f y) (hx : g x = f x) : ContinuousWithinAt g s x ↔ ContinuousWithinAt f s x

Full source

theorem continuousWithinAt_congr (h₁ : ∀ y ∈ s, g y = f y) (hx : g x = f x) :
    ContinuousWithinAtContinuousWithinAt g s x ↔ ContinuousWithinAt f s x :=
  ⟨fun h' ↦ h'.congr (fun x hx ↦ (h₁ x hx).symm) hx.symm, fun h' ↦  h'.congr h₁ hx⟩

Equivalence of Continuity Within Set at Point Under Pointwise Equality

Informal description

For functions $f$ and $g$ and a set $s$, if $g(y) = f(y)$ for all $y \in s$ and $g(x) = f(x)$, then $g$ is continuous within $s$ at $x$ if and only if $f$ is continuous within $s$ at $x$.

ContinuousWithinAt.congr_of_mem theorem

(h : ContinuousWithinAt f s x) (h₁ : ∀ y ∈ s, g y = f y) (hx : x ∈ s) : ContinuousWithinAt g s x

Full source

theorem ContinuousWithinAt.congr_of_mem (h : ContinuousWithinAt f s x)
    (h₁ : ∀ y ∈ s, g y = f y) (hx : x ∈ s) : ContinuousWithinAt g s x :=
  h.congr h₁ (h₁ x hx)

Continuity Within Set at Point Preserved by Pointwise Equality on Set

Informal description

Let $f$ be a function that is continuous within a set $s$ at a point $x \in s$. If $g$ is a function such that $g(y) = f(y)$ for all $y \in s$, then $g$ is also continuous within $s$ at $x$.

continuousWithinAt_congr_of_mem theorem

(h₁ : ∀ y ∈ s, g y = f y) (hx : x ∈ s) : ContinuousWithinAt g s x ↔ ContinuousWithinAt f s x

Full source

theorem continuousWithinAt_congr_of_mem (h₁ : ∀ y ∈ s, g y = f y) (hx : x ∈ s) :
    ContinuousWithinAtContinuousWithinAt g s x ↔ ContinuousWithinAt f s x :=
  continuousWithinAt_congr h₁ (h₁ x hx)

Equivalence of Continuity Within Set at Point Under Pointwise Equality on Set

Informal description

For functions $f$ and $g$ and a set $s$, if $g(y) = f(y)$ for all $y \in s$ and $x \in s$, then $g$ is continuous within $s$ at $x$ if and only if $f$ is continuous within $s$ at $x$.

ContinuousWithinAt.congr_of_insert theorem

(h : ContinuousWithinAt f s x) (h₁ : ∀ y ∈ insert x s, g y = f y) : ContinuousWithinAt g s x

Full source

theorem ContinuousWithinAt.congr_of_insert (h : ContinuousWithinAt f s x)
    (h₁ : ∀ y ∈ insert x s, g y = f y) : ContinuousWithinAt g s x :=
  h.congr (fun y hy ↦ h₁ y (mem_insert_of_mem _ hy)) (h₁ x (mem_insert _ _))

Continuity Within Set at Point Preserved by Pointwise Equality on Extended Set

Informal description

Let $f$ be a function that is continuous within a set $s$ at a point $x$. If $g$ is a function such that $g(y) = f(y)$ for all $y$ in the set $\{x\} \cup s$, then $g$ is also continuous within $s$ at $x$.

continuousWithinAt_congr_of_insert theorem

(h₁ : ∀ y ∈ insert x s, g y = f y) : ContinuousWithinAt g s x ↔ ContinuousWithinAt f s x

Full source

theorem continuousWithinAt_congr_of_insert
    (h₁ : ∀ y ∈ insert x s, g y = f y) :
    ContinuousWithinAtContinuousWithinAt g s x ↔ ContinuousWithinAt f s x :=
  continuousWithinAt_congr (fun y hy ↦ h₁ y (mem_insert_of_mem _ hy)) (h₁ x (mem_insert _ _))

Equivalence of Continuity Within Set at Point Under Pointwise Equality on Extended Set

Informal description

For functions $f$ and $g$ and a set $s$, if $g(y) = f(y)$ for all $y$ in the set $\{x\} \cup s$, then $g$ is continuous within $s$ at $x$ if and only if $f$ is continuous within $s$ at $x$.

ContinuousWithinAt.congr_mono theorem

(h : ContinuousWithinAt f s x) (h' : EqOn g f s₁) (h₁ : s₁ ⊆ s) (hx : g x = f x) : ContinuousWithinAt g s₁ x

Full source

theorem ContinuousWithinAt.congr_mono
    (h : ContinuousWithinAt f s x) (h' : EqOn g f s₁) (h₁ : s₁ ⊆ s) (hx : g x = f x) :
    ContinuousWithinAt g s₁ x :=
  (h.mono h₁).congr h' hx

Continuity Within Subset Preserved by Pointwise Equality on Subset and Point

Informal description

Let $f : \alpha \to \beta$ be a function between topological spaces, continuous within a set $s \subseteq \alpha$ at a point $x \in \alpha$. If $g : \alpha \to \beta$ coincides with $f$ on a subset $s_1 \subseteq s$ (i.e., $g(y) = f(y)$ for all $y \in s_1$) and satisfies $g(x) = f(x)$, then $g$ is continuous within $s_1$ at $x$.

ContinuousAt.congr_of_eventuallyEq theorem

(h : ContinuousAt f x) (hg : g =ᶠ[𝓝 x] f) : ContinuousAt g x

Full source

theorem ContinuousAt.congr_of_eventuallyEq (h : ContinuousAt f x) (hg : g =ᶠ[𝓝 x] f) :
    ContinuousAt g x := by
  simp only [← continuousWithinAt_univ] at h ⊢
  exact h.congr_of_eventuallyEq_of_mem (by rwa [nhdsWithin_univ]) (mem_univ x)

Continuity at a Point is Preserved by Eventual Equality

Informal description

Let $f : \alpha \to \beta$ be a function between topological spaces that is continuous at a point $x \in \alpha$. If $g : \alpha \to \beta$ is eventually equal to $f$ in the neighborhood filter of $x$ (i.e., $g$ and $f$ coincide on some neighborhood of $x$), then $g$ is also continuous at $x$.

ContinuousWithinAt.comp theorem

 {g : β → γ} {t : Set β} (hg : ContinuousWithinAt g t (f x)) (hf : ContinuousWithinAt f s x) (h : MapsTo f s t) :
  ContinuousWithinAt (g ∘ f) s x

Full source

theorem ContinuousWithinAt.comp {g : β → γ} {t : Set β}
    (hg : ContinuousWithinAt g t (f x)) (hf : ContinuousWithinAt f s x) (h : MapsTo f s t) :
    ContinuousWithinAt (g ∘ f) s x :=
  hg.tendsto.comp (hf.tendsto_nhdsWithin h)

Continuity of Composition Within Subsets

Informal description

Let $f : \alpha \to \beta$ and $g : \beta \to \gamma$ be functions, $x \in \alpha$ a point, and $s \subseteq \alpha$, $t \subseteq \beta$ sets. If $g$ is continuous within $t$ at $f(x)$, $f$ is continuous within $s$ at $x$, and $f$ maps $s$ into $t$, then the composition $g \circ f$ is continuous within $s$ at $x$.

ContinuousWithinAt.comp_of_eq theorem

 {g : β → γ} {t : Set β} {y : β} (hg : ContinuousWithinAt g t y) (hf : ContinuousWithinAt f s x) (h : MapsTo f s t)
  (hy : f x = y) : ContinuousWithinAt (g ∘ f) s x

Full source

theorem ContinuousWithinAt.comp_of_eq {g : β → γ} {t : Set β} {y : β}
    (hg : ContinuousWithinAt g t y) (hf : ContinuousWithinAt f s x) (h : MapsTo f s t)
    (hy : f x = y) : ContinuousWithinAt (g ∘ f) s x := by
  subst hy; exact hg.comp hf h

Continuity of Composition with Point Equality Condition

Informal description

Let $f : \alpha \to \beta$ and $g : \beta \to \gamma$ be functions between topological spaces, with $x \in \alpha$, $s \subseteq \alpha$, and $t \subseteq \beta$. If: 1. $g$ is continuous at $y$ within $t$, 2. $f$ is continuous at $x$ within $s$, 3. $f$ maps $s$ into $t$, and 4. $f(x) = y$, then the composition $g \circ f$ is continuous at $x$ within $s$.

ContinuousWithinAt.comp_inter theorem

 {g : β → γ} {t : Set β} (hg : ContinuousWithinAt g t (f x)) (hf : ContinuousWithinAt f s x) :
  ContinuousWithinAt (g ∘ f) (s ∩ f ⁻¹' t) x

Full source

theorem ContinuousWithinAt.comp_inter {g : β → γ} {t : Set β}
    (hg : ContinuousWithinAt g t (f x)) (hf : ContinuousWithinAt f s x) :
    ContinuousWithinAt (g ∘ f) (s ∩ f ⁻¹' t) x :=
  hg.comp (hf.mono inter_subset_left) inter_subset_right

Continuity of Composition on Intersection with Preimage

Informal description

Let $f : \alpha \to \beta$ and $g : \beta \to \gamma$ be functions between topological spaces, with $x \in \alpha$, $s \subseteq \alpha$, and $t \subseteq \beta$. If: 1. $g$ is continuous at $f(x)$ within $t$, and 2. $f$ is continuous at $x$ within $s$, then the composition $g \circ f$ is continuous at $x$ within $s \cap f^{-1}(t)$.

ContinuousWithinAt.comp_inter_of_eq theorem

 {g : β → γ} {t : Set β} {y : β} (hg : ContinuousWithinAt g t y) (hf : ContinuousWithinAt f s x) (hy : f x = y) :
  ContinuousWithinAt (g ∘ f) (s ∩ f ⁻¹' t) x

Full source

theorem ContinuousWithinAt.comp_inter_of_eq {g : β → γ} {t : Set β} {y : β}
    (hg : ContinuousWithinAt g t y) (hf : ContinuousWithinAt f s x) (hy : f x = y) :
    ContinuousWithinAt (g ∘ f) (s ∩ f ⁻¹' t) x := by
  subst hy; exact hg.comp_inter hf

Continuity of Composition on Intersection with Preimage under Point Equality Condition

Informal description

Let $f : \alpha \to \beta$ and $g : \beta \to \gamma$ be functions between topological spaces, with $x \in \alpha$, $s \subseteq \alpha$, and $t \subseteq \beta$. If: 1. $g$ is continuous at $y$ within $t$, 2. $f$ is continuous at $x$ within $s$, and 3. $f(x) = y$, then the composition $g \circ f$ is continuous at $x$ within $s \cap f^{-1}(t)$.

ContinuousWithinAt.comp_of_preimage_mem_nhdsWithin theorem

 {g : β → γ} {t : Set β} (hg : ContinuousWithinAt g t (f x)) (hf : ContinuousWithinAt f s x) (h : f ⁻¹' t ∈ 𝓝[s] x) :
  ContinuousWithinAt (g ∘ f) s x

Full source

theorem ContinuousWithinAt.comp_of_preimage_mem_nhdsWithin {g : β → γ} {t : Set β}
    (hg : ContinuousWithinAt g t (f x)) (hf : ContinuousWithinAt f s x) (h : f ⁻¹' tf ⁻¹' t ∈ 𝓝[s] x) :
    ContinuousWithinAt (g ∘ f) s x :=
  hg.tendsto.comp (tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within f hf h)

Continuity of Composition via Preimage Neighborhood Condition

Informal description

Let $f : \alpha \to \beta$ and $g : \beta \to \gamma$ be functions between topological spaces, with $x \in \alpha$, $s \subseteq \alpha$, and $t \subseteq \beta$. If: 1. $g$ is continuous at $f(x)$ within $t$, 2. $f$ is continuous at $x$ within $s$, and 3. the preimage $f^{-1}(t)$ is a neighborhood of $x$ within $s$, then the composition $g \circ f$ is continuous at $x$ within $s$.

ContinuousWithinAt.comp_of_preimage_mem_nhdsWithin_of_eq theorem

 {g : β → γ} {t : Set β} {y : β} (hg : ContinuousWithinAt g t y) (hf : ContinuousWithinAt f s x) (h : f ⁻¹' t ∈ 𝓝[s] x)
  (hy : f x = y) : ContinuousWithinAt (g ∘ f) s x

Full source

theorem ContinuousWithinAt.comp_of_preimage_mem_nhdsWithin_of_eq {g : β → γ} {t : Set β} {y : β}
    (hg : ContinuousWithinAt g t y) (hf : ContinuousWithinAt f s x) (h : f ⁻¹' tf ⁻¹' t ∈ 𝓝[s] x)
    (hy : f x = y) :
    ContinuousWithinAt (g ∘ f) s x := by
  subst hy; exact hg.comp_of_preimage_mem_nhdsWithin hf h

Continuity of Composition with Preimage Neighborhood and Point Condition

Informal description

Let $f : \alpha \to \beta$ and $g : \beta \to \gamma$ be functions between topological spaces, with $x \in \alpha$, $s \subseteq \alpha$, and $t \subseteq \beta$. If: 1. $g$ is continuous at $y$ within $t$, 2. $f$ is continuous at $x$ within $s$, 3. the preimage $f^{-1}(t)$ is a neighborhood of $x$ within $s$, and 4. $f(x) = y$, then the composition $g \circ f$ is continuous at $x$ within $s$.

ContinuousWithinAt.comp_of_mem_nhdsWithin_image theorem

 {g : β → γ} {t : Set β} (hg : ContinuousWithinAt g t (f x)) (hf : ContinuousWithinAt f s x) (hs : t ∈ 𝓝[f '' s] f x) :
  ContinuousWithinAt (g ∘ f) s x

Full source

theorem ContinuousWithinAt.comp_of_mem_nhdsWithin_image {g : β → γ} {t : Set β}
    (hg : ContinuousWithinAt g t (f x)) (hf : ContinuousWithinAt f s x)
    (hs : t ∈ 𝓝[f '' s] f x) : ContinuousWithinAt (g ∘ f) s x :=
  (hg.mono_of_mem_nhdsWithin hs).comp hf (mapsTo_image f s)

Continuity of Composition via Neighborhood Condition on Image

Informal description

Let $f : \alpha \to \beta$ and $g : \beta \to \gamma$ be functions between topological spaces, with $x \in \alpha$, $s \subseteq \alpha$, and $t \subseteq \beta$. If: 1. $g$ is continuous at $f(x)$ within $t$, 2. $f$ is continuous at $x$ within $s$, and 3. $t$ is a neighborhood of $f(x)$ within the image $f(s)$, then the composition $g \circ f$ is continuous at $x$ within $s$.

ContinuousWithinAt.comp_of_mem_nhdsWithin_image_of_eq theorem

 {g : β → γ} {t : Set β} {y : β} (hg : ContinuousWithinAt g t y) (hf : ContinuousWithinAt f s x) (hs : t ∈ 𝓝[f '' s] y)
  (hy : f x = y) : ContinuousWithinAt (g ∘ f) s x

Full source

theorem ContinuousWithinAt.comp_of_mem_nhdsWithin_image_of_eq {g : β → γ} {t : Set β} {y : β}
    (hg : ContinuousWithinAt g t y) (hf : ContinuousWithinAt f s x)
    (hs : t ∈ 𝓝[f '' s] y) (hy : f x = y) : ContinuousWithinAt (g ∘ f) s x := by
  subst hy; exact hg.comp_of_mem_nhdsWithin_image hf hs

Continuity of Composition with Neighborhood Condition on Image and Point Equality

Informal description

Let $f : \alpha \to \beta$ and $g : \beta \to \gamma$ be functions between topological spaces, with $x \in \alpha$, $s \subseteq \alpha$, and $t \subseteq \beta$. If: 1. $g$ is continuous at $y$ within $t$, 2. $f$ is continuous at $x$ within $s$, 3. $t$ is a neighborhood of $y$ within the image $f(s)$, and 4. $f(x) = y$, then the composition $g \circ f$ is continuous at $x$ within $s$.

ContinuousAt.comp_continuousWithinAt theorem

{g : β → γ} (hg : ContinuousAt g (f x)) (hf : ContinuousWithinAt f s x) : ContinuousWithinAt (g ∘ f) s x

Full source

theorem ContinuousAt.comp_continuousWithinAt {g : β → γ}
    (hg : ContinuousAt g (f x)) (hf : ContinuousWithinAt f s x) : ContinuousWithinAt (g ∘ f) s x :=
  hg.continuousWithinAt.comp hf (mapsTo_univ _ _)

Continuity of Composition via Pointwise and Relative Continuity

Informal description

Let $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$ be functions between topological spaces, $x \in \alpha$ a point, and $s \subseteq \alpha$ a subset. If $g$ is continuous at $f(x)$ and $f$ is continuous at $x$ within $s$, then the composition $g \circ f$ is continuous at $x$ within $s$.

ContinuousAt.comp_continuousWithinAt_of_eq theorem

 {g : β → γ} {y : β} (hg : ContinuousAt g y) (hf : ContinuousWithinAt f s x) (hy : f x = y) :
  ContinuousWithinAt (g ∘ f) s x

Full source

theorem ContinuousAt.comp_continuousWithinAt_of_eq {g : β → γ} {y : β}
    (hg : ContinuousAt g y) (hf : ContinuousWithinAt f s x) (hy : f x = y) :
    ContinuousWithinAt (g ∘ f) s x := by
  subst hy; exact hg.comp_continuousWithinAt hf

Composition of Continuous Functions with Point Equality

Informal description

Let $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$ be functions between topological spaces, with $x \in \alpha$, $s \subseteq \alpha$, and $y \in \beta$. If: 1. $g$ is continuous at $y$, 2. $f$ is continuous at $x$ within $s$, and 3. $f(x) = y$, then the composition $g \circ f$ is continuous at $x$ within $s$.

ContinuousOn.comp theorem

 {g : β → γ} {t : Set β} (hg : ContinuousOn g t) (hf : ContinuousOn f s) (h : MapsTo f s t) : ContinuousOn (g ∘ f) s

Full source

/-- See also `ContinuousOn.comp'` using the form `fun y ↦ g (f y)` instead of `g ∘ f`. -/
theorem ContinuousOn.comp {g : β → γ} {t : Set β} (hg : ContinuousOn g t)
    (hf : ContinuousOn f s) (h : MapsTo f s t) : ContinuousOn (g ∘ f) s := fun x hx =>
  ContinuousWithinAt.comp (hg _ (h hx)) (hf x hx) h

Continuity of Composition on Subsets

Informal description

Let $f : \alpha \to \beta$ and $g : \beta \to \gamma$ be functions, and let $s \subseteq \alpha$ and $t \subseteq \beta$ be subsets. If $g$ is continuous on $t$, $f$ is continuous on $s$, and $f$ maps $s$ into $t$, then the composition $g \circ f$ is continuous on $s$.

ContinuousOn.comp' theorem

 {g : β → γ} {f : α → β} {s : Set α} {t : Set β} (hg : ContinuousOn g t) (hf : ContinuousOn f s)
  (h : Set.MapsTo f s t) : ContinuousOn (fun x => g (f x)) s

Full source

/-- Variant of `ContinuousOn.comp` using the form `fun y ↦ g (f y)` instead of `g ∘ f`. -/
@[fun_prop]
theorem ContinuousOn.comp' {g : β → γ} {f : α → β} {s : Set α} {t : Set β} (hg : ContinuousOn g t)
    (hf : ContinuousOn f s) (h : Set.MapsTo f s t) : ContinuousOn (fun x => g (f x)) s :=
  ContinuousOn.comp hg hf h

Continuity of Pointwise Composition on Subsets

Informal description

Let $f : \alpha \to \beta$ and $g : \beta \to \gamma$ be functions, and let $s \subseteq \alpha$ and $t \subseteq \beta$ be subsets. If $g$ is continuous on $t$, $f$ is continuous on $s$, and $f$ maps $s$ into $t$, then the function $x \mapsto g(f(x))$ is continuous on $s$.

ContinuousOn.comp_inter theorem

 {g : β → γ} {t : Set β} (hg : ContinuousOn g t) (hf : ContinuousOn f s) : ContinuousOn (g ∘ f) (s ∩ f ⁻¹' t)

Full source

@[fun_prop]
theorem ContinuousOn.comp_inter {g : β → γ} {t : Set β} (hg : ContinuousOn g t)
    (hf : ContinuousOn f s) : ContinuousOn (g ∘ f) (s ∩ f ⁻¹' t) :=
  hg.comp (hf.mono inter_subset_left) inter_subset_right

Continuity of Composition on Intersection with Preimage

Informal description

Let $f : \alpha \to \beta$ and $g : \beta \to \gamma$ be functions, with $s \subseteq \alpha$ and $t \subseteq \beta$. If $g$ is continuous on $t$ and $f$ is continuous on $s$, then the composition $g \circ f$ is continuous on the intersection $s \cap f^{-1}(t)$.

Continuous.comp_continuousOn theorem

{g : β → γ} {f : α → β} {s : Set α} (hg : Continuous g) (hf : ContinuousOn f s) : ContinuousOn (g ∘ f) s

Full source

/-- See also `Continuous.comp_continuousOn'` using the form `fun y ↦ g (f y)`
instead of `g ∘ f`. -/
theorem Continuous.comp_continuousOn {g : β → γ} {f : α → β} {s : Set α} (hg : Continuous g)
    (hf : ContinuousOn f s) : ContinuousOn (g ∘ f) s :=
  hg.continuousOn.comp hf (mapsTo_univ _ _)

Composition of Continuous Function with Continuous-on-Subset Function

Informal description

Let $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$ be functions, with $s \subseteq \alpha$. If $g$ is continuous and $f$ is continuous on $s$, then the composition $g \circ f$ is continuous on $s$.

Continuous.comp_continuousOn' theorem

 {g : β → γ} {f : α → β} {s : Set α} (hg : Continuous g) (hf : ContinuousOn f s) : ContinuousOn (fun x ↦ g (f x)) s

Full source

/-- Variant of `Continuous.comp_continuousOn` using the form `fun y ↦ g (f y)`
instead of `g ∘ f`. -/
@[fun_prop]
theorem Continuous.comp_continuousOn' {g : β → γ} {f : α → β} {s : Set α} (hg : Continuous g)
    (hf : ContinuousOn f s) : ContinuousOn (fun x ↦ g (f x)) s :=
  hg.comp_continuousOn hf

Continuity of Pointwise Composition on Subset

Informal description

Let $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$ be functions, with $s \subseteq \alpha$. If $g$ is continuous and $f$ is continuous on $s$, then the function $x \mapsto g(f(x))$ is continuous on $s$.

ContinuousOn.comp_continuous theorem

 {g : β → γ} {f : α → β} {s : Set β} (hg : ContinuousOn g s) (hf : Continuous f) (hs : ∀ x, f x ∈ s) :
  Continuous (g ∘ f)

Full source

theorem ContinuousOn.comp_continuous {g : β → γ} {f : α → β} {s : Set β} (hg : ContinuousOn g s)
    (hf : Continuous f) (hs : ∀ x, f x ∈ s) : Continuous (g ∘ f) := by
  rw [continuous_iff_continuousOn_univ] at *
  exact hg.comp hf fun x _ => hs x

Continuity of Composition with Continuous Function and Continuous-on-Subset Function

Informal description

Let $f \colon \alpha \to \beta$ be a continuous function and $g \colon \beta \to \gamma$ be a function continuous on a subset $s \subseteq \beta$. If $f(x) \in s$ for all $x \in \alpha$, then the composition $g \circ f \colon \alpha \to \gamma$ is continuous.

ContinuousOn.image_comp_continuous theorem

 {g : β → γ} {f : α → β} {s : Set α} (hg : ContinuousOn g (f '' s)) (hf : Continuous f) : ContinuousOn (g ∘ f) s

Full source

theorem ContinuousOn.image_comp_continuous {g : β → γ} {f : α → β} {s : Set α}
    (hg : ContinuousOn g (f '' s)) (hf : Continuous f) : ContinuousOn (g ∘ f) s :=
  hg.comp hf.continuousOn (s.mapsTo_image f)

Continuity of Composition via Image Continuity

Informal description

Let $f \colon \alpha \to \beta$ be a continuous function and $g \colon \beta \to \gamma$ be a function continuous on the image $f(s) \subseteq \beta$ of a subset $s \subseteq \alpha$. Then the composition $g \circ f$ is continuous on $s$.

ContinuousAt.comp₂_continuousWithinAt theorem

 {f : β × γ → δ} {g : α → β} {h : α → γ} {x : α} {s : Set α} (hf : ContinuousAt f (g x, h x))
  (hg : ContinuousWithinAt g s x) (hh : ContinuousWithinAt h s x) : ContinuousWithinAt (fun x ↦ f (g x, h x)) s x

Full source

theorem ContinuousAt.comp₂_continuousWithinAt {f : β × γ → δ} {g : α → β} {h : α → γ} {x : α}
    {s : Set α} (hf : ContinuousAt f (g x, h x)) (hg : ContinuousWithinAt g s x)
    (hh : ContinuousWithinAt h s x) :
    ContinuousWithinAt (fun x ↦ f (g x, h x)) s x :=
  ContinuousAt.comp_continuousWithinAt hf (hg.prodMk_nhds hh)

Continuity of Binary Composition via Pointwise and Relative Continuity

Informal description

Let $f \colon \beta \times \gamma \to \delta$ be a function between topological spaces, and let $g \colon \alpha \to \beta$ and $h \colon \alpha \to \gamma$ be functions. For a point $x \in \alpha$ and a subset $s \subseteq \alpha$, if $f$ is continuous at $(g(x), h(x))$, and both $g$ and $h$ are continuous at $x$ within $s$, then the function $x \mapsto f(g(x), h(x))$ is continuous at $x$ within $s$.

ContinuousAt.comp₂_continuousWithinAt_of_eq theorem

 {f : β × γ → δ} {g : α → β} {h : α → γ} {x : α} {s : Set α} {y : β × γ} (hf : ContinuousAt f y)
  (hg : ContinuousWithinAt g s x) (hh : ContinuousWithinAt h s x) (e : (g x, h x) = y) :
  ContinuousWithinAt (fun x ↦ f (g x, h x)) s x

Full source

theorem ContinuousAt.comp₂_continuousWithinAt_of_eq {f : β × γ → δ} {g : α → β}
    {h : α → γ} {x : α} {s : Set α} {y : β × γ} (hf : ContinuousAt f y)
    (hg : ContinuousWithinAt g s x) (hh : ContinuousWithinAt h s x) (e : (g x, h x) = y) :
    ContinuousWithinAt (fun x ↦ f (g x, h x)) s x := by
  rw [← e] at hf
  exact hf.comp₂_continuousWithinAt hg hh

Continuity of Binary Composition via Pointwise and Relative Continuity with Equality Condition

Informal description

Let $f \colon \beta \times \gamma \to \delta$ be a function between topological spaces, and let $g \colon \alpha \to \beta$ and $h \colon \alpha \to \gamma$ be functions. For a point $x \in \alpha$, a subset $s \subseteq \alpha$, and a point $y \in \beta \times \gamma$, if $f$ is continuous at $y$, both $g$ and $h$ are continuous at $x$ within $s$, and $(g(x), h(x)) = y$, then the function $x \mapsto f(g(x), h(x))$ is continuous at $x$ within $s$.

ContinuousWithinAt.mem_closure_image theorem

(h : ContinuousWithinAt f s x) (hx : x ∈ closure s) : f x ∈ closure (f '' s)

Full source

theorem ContinuousWithinAt.mem_closure_image
    (h : ContinuousWithinAt f s x) (hx : x ∈ closure s) : f x ∈ closure (f '' s) :=
  haveI := mem_closure_iff_nhdsWithin_neBot.1 hx
  mem_closure_of_tendsto h <| mem_of_superset self_mem_nhdsWithin (subset_preimage_image f s)

Image of Point in Closure under ContinuousWithinAt Belongs to Closure of Image

Informal description

Let $f : \alpha \to \beta$ be a function between topological spaces, $s \subseteq \alpha$ a subset, and $x \in \alpha$ a point. If $f$ is continuous within $s$ at $x$ and $x$ belongs to the closure of $s$, then the image $f(x)$ belongs to the closure of the image $f(s)$.

ContinuousWithinAt.mem_closure theorem

{t : Set β} (h : ContinuousWithinAt f s x) (hx : x ∈ closure s) (ht : MapsTo f s t) : f x ∈ closure t

Full source

theorem ContinuousWithinAt.mem_closure {t : Set β}
    (h : ContinuousWithinAt f s x) (hx : x ∈ closure s) (ht : MapsTo f s t) : f x ∈ closure t :=
  closure_mono (image_subset_iff.2 ht) (h.mem_closure_image hx)

Closure Preservation under ContinuousWithinAt and MapsTo

Informal description

Let $f : \alpha \to \beta$ be a function between topological spaces, $s \subseteq \alpha$ a subset, $x \in \alpha$ a point, and $t \subseteq \beta$ a subset. If $f$ is continuous within $s$ at $x$, $x$ belongs to the closure of $s$, and $f$ maps $s$ into $t$, then $f(x)$ belongs to the closure of $t$.

Set.MapsTo.closure_of_continuousWithinAt theorem

{t : Set β} (h : MapsTo f s t) (hc : ∀ x ∈ closure s, ContinuousWithinAt f s x) : MapsTo f (closure s) (closure t)

Full source

theorem Set.MapsTo.closure_of_continuousWithinAt {t : Set β}
    (h : MapsTo f s t) (hc : ∀ x ∈ closure s, ContinuousWithinAt f s x) :
    MapsTo f (closure s) (closure t) := fun x hx => (hc x hx).mem_closure hx h

Closure Preservation under ContinuousWithinAt on Closure

Informal description

Let $f : \alpha \to \beta$ be a function between topological spaces, $s \subseteq \alpha$ a subset, and $t \subseteq \beta$ a subset. If $f$ maps $s$ into $t$ and $f$ is continuous within $s$ at every point in the closure of $s$, then $f$ maps the closure of $s$ into the closure of $t$.

Set.MapsTo.closure_of_continuousOn theorem

{t : Set β} (h : MapsTo f s t) (hc : ContinuousOn f (closure s)) : MapsTo f (closure s) (closure t)

Full source

theorem Set.MapsTo.closure_of_continuousOn {t : Set β} (h : MapsTo f s t)
    (hc : ContinuousOn f (closure s)) : MapsTo f (closure s) (closure t) :=
  h.closure_of_continuousWithinAt fun x hx => (hc x hx).mono subset_closure

Closure Preservation under Continuous Function on Closure

Informal description

Let $f : \alpha \to \beta$ be a function between topological spaces, $s \subseteq \alpha$ a subset, and $t \subseteq \beta$ a subset. If $f$ maps $s$ into $t$ and $f$ is continuous on the closure of $s$, then $f$ maps the closure of $s$ into the closure of $t$.

ContinuousWithinAt.image_closure theorem

(hf : ∀ x ∈ closure s, ContinuousWithinAt f s x) : f '' closure s ⊆ closure (f '' s)

Full source

theorem ContinuousWithinAt.image_closure
    (hf : ∀ x ∈ closure s, ContinuousWithinAt f s x) : f '' closure sf '' closure s ⊆ closure (f '' s) :=
  ((mapsTo_image f s).closure_of_continuousWithinAt hf).image_subset

Image of Closure under ContinuousWithinAt is Contained in Closure of Image

Informal description

Let $f : \alpha \to \beta$ be a function between topological spaces and $s \subseteq \alpha$ a subset. If $f$ is continuous within $s$ at every point in the closure of $s$, then the image of the closure of $s$ under $f$ is contained in the closure of the image of $s$ under $f$, i.e., $f(\overline{s}) \subseteq \overline{f(s)}$.

ContinuousOn.image_closure theorem

(hf : ContinuousOn f (closure s)) : f '' closure s ⊆ closure (f '' s)

Full source

theorem ContinuousOn.image_closure (hf : ContinuousOn f (closure s)) :
    f '' closure sf '' closure s ⊆ closure (f '' s) :=
  ContinuousWithinAt.image_closure fun x hx => (hf x hx).mono subset_closure

Image of Closure under Continuous Function is Contained in Closure of Image

Informal description

Let $f : \alpha \to \beta$ be a function between topological spaces and $s \subseteq \alpha$ a subset. If $f$ is continuous on the closure of $s$, then the image of the closure of $s$ under $f$ is contained in the closure of the image of $s$ under $f$, i.e., $f(\overline{s}) \subseteq \overline{f(s)}$.

ContinuousWithinAt.prodMk theorem

 {f : α → β} {g : α → γ} {s : Set α} {x : α} (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) :
  ContinuousWithinAt (fun x => (f x, g x)) s x

Full source

theorem ContinuousWithinAt.prodMk {f : α → β} {g : α → γ} {s : Set α} {x : α}
    (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) :
    ContinuousWithinAt (fun x => (f x, g x)) s x :=
  hf.prodMk_nhds hg

Continuity Within a Set is Preserved Under Product of Functions

Informal description

Let $f : \alpha \to \beta$ and $g : \alpha \to \gamma$ be functions, $s \subseteq \alpha$ a subset, and $x \in \alpha$ a point. If $f$ is continuous within $s$ at $x$ and $g$ is continuous within $s$ at $x$, then the product function $x \mapsto (f(x), g(x))$ is continuous within $s$ at $x$.

ContinuousOn.prodMk theorem

 {f : α → β} {g : α → γ} {s : Set α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
  ContinuousOn (fun x => (f x, g x)) s

Full source

@[fun_prop]
theorem ContinuousOn.prodMk {f : α → β} {g : α → γ} {s : Set α} (hf : ContinuousOn f s)
    (hg : ContinuousOn g s) : ContinuousOn (fun x => (f x, g x)) s := fun x hx =>
  (hf x hx).prodMk (hg x hx)

Continuity of Product Function on a Set

Informal description

Let $f : \alpha \to \beta$ and $g : \alpha \to \gamma$ be functions and $s \subseteq \alpha$ a subset. If $f$ is continuous on $s$ and $g$ is continuous on $s$, then the product function $x \mapsto (f(x), g(x))$ is continuous on $s$.

continuousOn_fst theorem

{s : Set (α × β)} : ContinuousOn Prod.fst s

Full source

theorem continuousOn_fst {s : Set (α × β)} : ContinuousOn Prod.fst s :=
  continuous_fst.continuousOn

Continuity of First Projection on Subsets of Product Space

Informal description

For any subset $s$ of the product space $\alpha \times \beta$, the projection map $\mathrm{fst} \colon \alpha \times \beta \to \alpha$ is continuous on $s$.

continuousWithinAt_fst theorem

{s : Set (α × β)} {p : α × β} : ContinuousWithinAt Prod.fst s p

Full source

theorem continuousWithinAt_fst {s : Set (α × β)} {p : α × β} : ContinuousWithinAt Prod.fst s p :=
  continuous_fst.continuousWithinAt

Continuity of First Projection Within Subset at Point

Informal description

For any subset $s$ of the product space $\alpha \times \beta$ and any point $p \in \alpha \times \beta$, the first projection map $\mathrm{fst} \colon \alpha \times \beta \to \alpha$ is continuous within $s$ at $p$.

ContinuousOn.fst theorem

{f : α → β × γ} {s : Set α} (hf : ContinuousOn f s) : ContinuousOn (fun x => (f x).1) s

Full source

@[fun_prop]
theorem ContinuousOn.fst {f : α → β × γ} {s : Set α} (hf : ContinuousOn f s) :
    ContinuousOn (fun x => (f x).1) s :=
  continuous_fst.comp_continuousOn hf

Continuity of First Projection under Continuous Function on Subset

Informal description

Let $f \colon \alpha \to \beta \times \gamma$ be a function and $s \subseteq \alpha$. If $f$ is continuous on $s$, then the first projection function $x \mapsto (f(x)).1$ is also continuous on $s$.

ContinuousWithinAt.fst theorem

 {f : α → β × γ} {s : Set α} {a : α} (h : ContinuousWithinAt f s a) : ContinuousWithinAt (fun x => (f x).fst) s a

Full source

theorem ContinuousWithinAt.fst {f : α → β × γ} {s : Set α} {a : α} (h : ContinuousWithinAt f s a) :
    ContinuousWithinAt (fun x => (f x).fst) s a :=
  continuousAt_fst.comp_continuousWithinAt h

Continuity of First Projection under Relative Continuity

Informal description

Let $f \colon \alpha \to \beta \times \gamma$ be a function between topological spaces, $s \subseteq \alpha$ a subset, and $a \in \alpha$ a point. If $f$ is continuous at $a$ within $s$, then the first projection function $x \mapsto (f(x)).1$ is also continuous at $a$ within $s$.

continuousOn_snd theorem

{s : Set (α × β)} : ContinuousOn Prod.snd s

Full source

theorem continuousOn_snd {s : Set (α × β)} : ContinuousOn Prod.snd s :=
  continuous_snd.continuousOn

Continuity of Second Projection on Subsets of Product Space

Informal description

For any subset $s$ of the product space $\alpha \times \beta$, the projection function $\operatorname{snd} \colon \alpha \times \beta \to \beta$ is continuous on $s$.

continuousWithinAt_snd theorem

{s : Set (α × β)} {p : α × β} : ContinuousWithinAt Prod.snd s p

Full source

theorem continuousWithinAt_snd {s : Set (α × β)} {p : α × β} : ContinuousWithinAt Prod.snd s p :=
  continuous_snd.continuousWithinAt

Continuity of Second Projection Within Subset at Point in Product Space

Informal description

For any subset $s$ of the product space $\alpha \times \beta$ and any point $p \in \alpha \times \beta$, the second projection function $\operatorname{snd} \colon \alpha \times \beta \to \beta$ is continuous within $s$ at $p$.

ContinuousOn.snd theorem

{f : α → β × γ} {s : Set α} (hf : ContinuousOn f s) : ContinuousOn (fun x => (f x).2) s

Full source

@[fun_prop]
theorem ContinuousOn.snd {f : α → β × γ} {s : Set α} (hf : ContinuousOn f s) :
    ContinuousOn (fun x => (f x).2) s :=
  continuous_snd.comp_continuousOn hf

Continuity of Second Projection under Continuous Function on Subset

Informal description

Let $f \colon \alpha \to \beta \times \gamma$ be a function and $s \subseteq \alpha$ a subset. If $f$ is continuous on $s$, then the second projection function $x \mapsto (f(x)).2$ is continuous on $s$.

ContinuousWithinAt.snd theorem

 {f : α → β × γ} {s : Set α} {a : α} (h : ContinuousWithinAt f s a) : ContinuousWithinAt (fun x => (f x).snd) s a

Full source

theorem ContinuousWithinAt.snd {f : α → β × γ} {s : Set α} {a : α} (h : ContinuousWithinAt f s a) :
    ContinuousWithinAt (fun x => (f x).snd) s a :=
  continuousAt_snd.comp_continuousWithinAt h

Continuity of Second Projection under Relative Continuity

Informal description

Let $f \colon \alpha \to \beta \times \gamma$ be a function between topological spaces, $s \subseteq \alpha$ a subset, and $a \in \alpha$ a point. If $f$ is continuous at $a$ within $s$, then the second projection $\mathrm{snd} \circ f$ (i.e., the function $x \mapsto (f(x)).2$) is also continuous at $a$ within $s$.

continuousWithinAt_prod_iff theorem

 {f : α → β × γ} {s : Set α} {x : α} :
  ContinuousWithinAt f s x ↔ ContinuousWithinAt (Prod.fst ∘ f) s x ∧ ContinuousWithinAt (Prod.snd ∘ f) s x

Full source

theorem continuousWithinAt_prod_iff {f : α → β × γ} {s : Set α} {x : α} :
    ContinuousWithinAtContinuousWithinAt f s x ↔
      ContinuousWithinAt (Prod.fst ∘ f) s x ∧ ContinuousWithinAt (Prod.snd ∘ f) s x :=
  ⟨fun h => ⟨h.fst, h.snd⟩, fun ⟨h1, h2⟩ => h1.prodMk h2⟩

Characterization of Continuity Within a Set via Component Functions

Informal description

Let $f \colon \alpha \to \beta \times \gamma$ be a function, $s \subseteq \alpha$ a subset, and $x \in \alpha$ a point. Then $f$ is continuous at $x$ within $s$ if and only if both the first projection $x \mapsto (f(x)).1$ and the second projection $x \mapsto (f(x)).2$ are continuous at $x$ within $s$.

ContinuousWithinAt.prodMap theorem

 {f : α → γ} {g : β → δ} {s : Set α} {t : Set β} {x : α} {y : β} (hf : ContinuousWithinAt f s x)
  (hg : ContinuousWithinAt g t y) : ContinuousWithinAt (Prod.map f g) (s ×ˢ t) (x, y)

Full source

theorem ContinuousWithinAt.prodMap {f : α → γ} {g : β → δ} {s : Set α} {t : Set β} {x : α} {y : β}
    (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g t y) :
    ContinuousWithinAt (Prod.map f g) (s ×ˢ t) (x, y) :=
  .prodMk (hf.comp continuousWithinAt_fst mapsTo_fst_prod)
    (hg.comp continuousWithinAt_snd mapsTo_snd_prod)

Continuity of Product Map Within Product Subset at Point

Informal description

Let $f \colon \alpha \to \gamma$ and $g \colon \beta \to \delta$ be functions between topological spaces, with $s \subseteq \alpha$, $t \subseteq \beta$ subsets, and $x \in \alpha$, $y \in \beta$ points. If $f$ is continuous within $s$ at $x$ and $g$ is continuous within $t$ at $y$, then the product map $(f, g) \colon \alpha \times \beta \to \gamma \times \delta$ is continuous within the product set $s \times t$ at the point $(x, y)$.

ContinuousOn.prodMap theorem

 {f : α → γ} {g : β → δ} {s : Set α} {t : Set β} (hf : ContinuousOn f s) (hg : ContinuousOn g t) :
  ContinuousOn (Prod.map f g) (s ×ˢ t)

Full source

theorem ContinuousOn.prodMap {f : α → γ} {g : β → δ} {s : Set α} {t : Set β} (hf : ContinuousOn f s)
    (hg : ContinuousOn g t) : ContinuousOn (Prod.map f g) (s ×ˢ t) := fun ⟨x, y⟩ ⟨hx, hy⟩ =>
  (hf x hx).prodMap (hg y hy)

Continuity of Product Map on Product Subset

Informal description

Let $f \colon \alpha \to \gamma$ and $g \colon \beta \to \delta$ be functions between topological spaces, with $s \subseteq \alpha$ and $t \subseteq \beta$ subsets. If $f$ is continuous on $s$ and $g$ is continuous on $t$, then the product map $(f, g) \colon \alpha \times \beta \to \gamma \times \delta$ is continuous on the product set $s \times t$.

continuousWithinAt_prod_of_discrete_left theorem

 [DiscreteTopology α] {f : α × β → γ} {s : Set (α × β)} {x : α × β} :
  ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ⟨x.1, ·⟩) {b | (x.1, b) ∈ s} x.2

Full source

theorem continuousWithinAt_prod_of_discrete_left [DiscreteTopology α]
    {f : α × β → γ} {s : Set (α × β)} {x : α × β} :
    ContinuousWithinAtContinuousWithinAt f s x ↔ ContinuousWithinAt (f ⟨x.1, ·⟩) {b | (x.1, b) ∈ s} x.2 := by
  rw [← x.eta]; simp_rw [ContinuousWithinAt, nhdsWithin, nhds_prod_eq, nhds_discrete, pure_prod,
    ← map_inf_principal_preimage]; rfl

Continuity Within Product at Discrete Component

Informal description

Let $α$ be a topological space with the discrete topology, $β$ and $γ$ be topological spaces, $f : α × β → γ$ a function, $s ⊆ α × β$ a subset, and $x = (x_1, x_2) ∈ α × β$ a point. Then $f$ is continuous within $s$ at $x$ if and only if the partially applied function $b ↦ f(x_1, b)$ is continuous within $\{b ∈ β ∣ (x_1, b) ∈ s\}$ at $x_2$.

continuousWithinAt_prod_of_discrete_right theorem

 [DiscreteTopology β] {f : α × β → γ} {s : Set (α × β)} {x : α × β} :
  ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ⟨·, x.2⟩) {a | (a, x.2) ∈ s} x.1

Full source

theorem continuousWithinAt_prod_of_discrete_right [DiscreteTopology β]
    {f : α × β → γ} {s : Set (α × β)} {x : α × β} :
    ContinuousWithinAtContinuousWithinAt f s x ↔ ContinuousWithinAt (f ⟨·, x.2⟩) {a | (a, x.2) ∈ s} x.1 := by
  rw [← x.eta]; simp_rw [ContinuousWithinAt, nhdsWithin, nhds_prod_eq, nhds_discrete, prod_pure,
    ← map_inf_principal_preimage]; rfl

Continuity Within Product Set for Discrete Right Factor

Informal description

Let $β$ be a discrete topological space, $f : α × β → γ$ a function, $s$ a subset of $α × β$, and $x = (x_1, x_2)$ a point in $α × β$. Then $f$ is continuous within $s$ at $x$ if and only if the partially applied function $f(·, x_2)$ is continuous within $\{a ∈ α \mid (a, x_2) ∈ s\}$ at $x_1$.

continuousAt_prod_of_discrete_left theorem

[DiscreteTopology α] {f : α × β → γ} {x : α × β} : ContinuousAt f x ↔ ContinuousAt (f ⟨x.1, ·⟩) x.2

Full source

theorem continuousAt_prod_of_discrete_left [DiscreteTopology α] {f : α × β → γ} {x : α × β} :
    ContinuousAtContinuousAt f x ↔ ContinuousAt (f ⟨x.1, ·⟩) x.2 := by
  simp_rw [← continuousWithinAt_univ]; exact continuousWithinAt_prod_of_discrete_left

Continuity at Product Point with Discrete Left Factor

Informal description

Let $α$ be a topological space with the discrete topology, $β$ and $γ$ be topological spaces, $f : α × β → γ$ a function, and $x = (x_1, x_2) ∈ α × β$ a point. Then $f$ is continuous at $x$ if and only if the partially applied function $b ↦ f(x_1, b)$ is continuous at $x_2$.

continuousAt_prod_of_discrete_right theorem

[DiscreteTopology β] {f : α × β → γ} {x : α × β} : ContinuousAt f x ↔ ContinuousAt (f ⟨·, x.2⟩) x.1

Full source

theorem continuousAt_prod_of_discrete_right [DiscreteTopology β] {f : α × β → γ} {x : α × β} :
    ContinuousAtContinuousAt f x ↔ ContinuousAt (f ⟨·, x.2⟩) x.1 := by
  simp_rw [← continuousWithinAt_univ]; exact continuousWithinAt_prod_of_discrete_right

Continuity at Product Point for Discrete Right Factor

Informal description

Let $β$ be a discrete topological space, $f : α × β → γ$ a function, and $x = (x_1, x_2)$ a point in $α × β$. Then $f$ is continuous at $x$ if and only if the partially applied function $f(·, x_2)$ is continuous at $x_1$.

continuousOn_prod_of_discrete_left theorem

 [DiscreteTopology α] {f : α × β → γ} {s : Set (α × β)} :
  ContinuousOn f s ↔ ∀ a, ContinuousOn (f ⟨a, ·⟩) {b | (a, b) ∈ s}

Full source

theorem continuousOn_prod_of_discrete_left [DiscreteTopology α] {f : α × β → γ} {s : Set (α × β)} :
    ContinuousOnContinuousOn f s ↔ ∀ a, ContinuousOn (f ⟨a, ·⟩) {b | (a, b) ∈ s} := by
  simp_rw [ContinuousOn, Prod.forall, continuousWithinAt_prod_of_discrete_left]; rfl

Continuity on Product Space with Discrete Left Factor

Informal description

Let $α$ be a topological space with the discrete topology, and let $f : α × β → γ$ be a function defined on the product space $α × β$. For any subset $s$ of $α × β$, the function $f$ is continuous on $s$ if and only if for every $a ∈ α$, the function $f(a, \cdot)$ is continuous on the set $\{b ∈ β \mid (a, b) ∈ s\}$.

continuousOn_prod_of_discrete_right theorem

 [DiscreteTopology β] {f : α × β → γ} {s : Set (α × β)} :
  ContinuousOn f s ↔ ∀ b, ContinuousOn (f ⟨·, b⟩) {a | (a, b) ∈ s}

Full source

theorem continuousOn_prod_of_discrete_right [DiscreteTopology β] {f : α × β → γ} {s : Set (α × β)} :
    ContinuousOnContinuousOn f s ↔ ∀ b, ContinuousOn (f ⟨·, b⟩) {a | (a, b) ∈ s} := by
  simp_rw [ContinuousOn, Prod.forall, continuousWithinAt_prod_of_discrete_right]; apply forall_swap

Continuity on Product Space with Discrete Right Factor

Informal description

Let $\beta$ be a topological space with the discrete topology, and let $f : \alpha \times \beta \to \gamma$ be a function defined on the product space $\alpha \times \beta$. For any subset $s$ of $\alpha \times \beta$, the function $f$ is continuous on $s$ if and only if for every $b \in \beta$, the function $f(\cdot, b)$ is continuous on the set $\{a \in \alpha \mid (a, b) \in s\}$.

continuous_prod_of_discrete_left theorem

[DiscreteTopology α] {f : α × β → γ} : Continuous f ↔ ∀ a, Continuous (f ⟨a, ·⟩)

Full source

/-- If a function `f a b` is such that `y ↦ f a b` is continuous for all `a`, and `a` lives in a
discrete space, then `f` is continuous, and vice versa. -/
theorem continuous_prod_of_discrete_left [DiscreteTopology α] {f : α × β → γ} :
    ContinuousContinuous f ↔ ∀ a, Continuous (f ⟨a, ·⟩) := by
  simp_rw [continuous_iff_continuousOn_univ]; exact continuousOn_prod_of_discrete_left

Continuity Criterion for Functions on Product Space with Discrete Left Factor

Informal description

Let $α$ be a topological space with the discrete topology and $f : α × β → γ$ be a function. Then $f$ is continuous if and only if for every $a ∈ α$, the function $b ↦ f(a, b)$ is continuous.

continuous_prod_of_discrete_right theorem

[DiscreteTopology β] {f : α × β → γ} : Continuous f ↔ ∀ b, Continuous (f ⟨·, b⟩)

Full source

theorem continuous_prod_of_discrete_right [DiscreteTopology β] {f : α × β → γ} :
    ContinuousContinuous f ↔ ∀ b, Continuous (f ⟨·, b⟩) := by
  simp_rw [continuous_iff_continuousOn_univ]; exact continuousOn_prod_of_discrete_right

Continuity Criterion for Functions on Product Space with Discrete Right Factor

Informal description

Let $\beta$ be a topological space with the discrete topology and $f : \alpha \times \beta \to \gamma$ be a function. Then $f$ is continuous if and only if for every $b \in \beta$, the function $a \mapsto f(a, b)$ is continuous.

isOpenMap_prod_of_discrete_left theorem

[DiscreteTopology α] {f : α × β → γ} : IsOpenMap f ↔ ∀ a, IsOpenMap (f ⟨a, ·⟩)

Full source

theorem isOpenMap_prod_of_discrete_left [DiscreteTopology α] {f : α × β → γ} :
    IsOpenMapIsOpenMap f ↔ ∀ a, IsOpenMap (f ⟨a, ·⟩) := by
  simp_rw [isOpenMap_iff_nhds_le, Prod.forall, nhds_prod_eq, nhds_discrete, pure_prod, map_map]
  rfl

Open Map Characterization for Product Space with Discrete Left Factor

Informal description

Let $α$ be a topological space with the discrete topology, and let $f : α × β → γ$ be a function. Then $f$ is an open map if and only if for every $a ∈ α$, the function $f(a, \cdot) : β → γ$ is an open map.

isOpenMap_prod_of_discrete_right theorem

[DiscreteTopology β] {f : α × β → γ} : IsOpenMap f ↔ ∀ b, IsOpenMap (f ⟨·, b⟩)

Full source

theorem isOpenMap_prod_of_discrete_right [DiscreteTopology β] {f : α × β → γ} :
    IsOpenMapIsOpenMap f ↔ ∀ b, IsOpenMap (f ⟨·, b⟩) := by
  simp_rw [isOpenMap_iff_nhds_le, Prod.forall, forall_swap (α := α) (β := β), nhds_prod_eq,
    nhds_discrete, prod_pure, map_map]; rfl

Open Map Criterion for Product Space with Discrete Right Factor

Informal description

Let $\beta$ be a topological space with the discrete topology and $f : \alpha \times \beta \to \gamma$ be a function. Then $f$ is an open map if and only if for every $b \in \beta$, the partial function $f(\cdot, b) : \alpha \to \gamma$ is an open map.

continuousWithinAt_pi theorem

 {ι : Type*} {π : ι → Type*} [∀ i, TopologicalSpace (π i)] {f : α → ∀ i, π i} {s : Set α} {x : α} :
  ContinuousWithinAt f s x ↔ ∀ i, ContinuousWithinAt (fun y => f y i) s x

Full source

theorem continuousWithinAt_pi {ι : Type*} {π : ι → Type*} [∀ i, TopologicalSpace (π i)]
    {f : α → ∀ i, π i} {s : Set α} {x : α} :
    ContinuousWithinAtContinuousWithinAt f s x ↔ ∀ i, ContinuousWithinAt (fun y => f y i) s x :=
  tendsto_pi_nhds

Coordinate-wise Continuity Within a Set at a Point for Product Spaces

Informal description

Let $\alpha$ be a topological space, $\{\pi_i\}_{i \in \iota}$ be a family of topological spaces indexed by $\iota$, $f: \alpha \to \prod_{i \in \iota} \pi_i$ be a function, $s \subseteq \alpha$ be a subset, and $x \in \alpha$ be a point. Then $f$ is continuous within $s$ at $x$ if and only if for each index $i \in \iota$, the coordinate function $y \mapsto f(y)_i$ is continuous within $s$ at $x$.

continuousOn_pi theorem

 {ι : Type*} {π : ι → Type*} [∀ i, TopologicalSpace (π i)] {f : α → ∀ i, π i} {s : Set α} :
  ContinuousOn f s ↔ ∀ i, ContinuousOn (fun y => f y i) s

Full source

theorem continuousOn_pi {ι : Type*} {π : ι → Type*} [∀ i, TopologicalSpace (π i)]
    {f : α → ∀ i, π i} {s : Set α} : ContinuousOnContinuousOn f s ↔ ∀ i, ContinuousOn (fun y => f y i) s :=
  ⟨fun h i x hx => tendsto_pi_nhds.1 (h x hx) i, fun h x hx => tendsto_pi_nhds.2 fun i => h i x hx⟩

Componentwise Continuity Criterion for Functions on Product Spaces

Informal description

Let $\{ \pi_i \}_{i \in \iota}$ be a family of topological spaces, $f : \alpha \to \prod_{i \in \iota} \pi_i$ a function, and $s \subseteq \alpha$ a subset. Then $f$ is continuous on $s$ if and only if for every index $i \in \iota$, the component function $y \mapsto f(y)_i$ is continuous on $s$.

continuousOn_pi' theorem

 {ι : Type*} {π : ι → Type*} [∀ i, TopologicalSpace (π i)] {f : α → ∀ i, π i} {s : Set α}
  (hf : ∀ i, ContinuousOn (fun y => f y i) s) : ContinuousOn f s

Full source

@[fun_prop]
theorem continuousOn_pi' {ι : Type*} {π : ι → Type*} [∀ i, TopologicalSpace (π i)]
    {f : α → ∀ i, π i} {s : Set α} (hf : ∀ i, ContinuousOn (fun y => f y i) s) :
    ContinuousOn f s :=
  continuousOn_pi.2 hf

Componentwise Continuity Implies Continuity on Product Spaces

Informal description

Let $\{ \pi_i \}_{i \in \iota}$ be a family of topological spaces, $f : \alpha \to \prod_{i \in \iota} \pi_i$ a function, and $s \subseteq \alpha$ a subset. If for every index $i \in \iota$, the component function $y \mapsto f(y)_i$ is continuous on $s$, then $f$ is continuous on $s$.

continuousOn_apply theorem

 {ι : Type*} {π : ι → Type*} [∀ i, TopologicalSpace (π i)] (i : ι) (s) : ContinuousOn (fun p : ∀ i, π i => p i) s

Full source

@[fun_prop]
theorem continuousOn_apply {ι : Type*} {π : ι → Type*} [∀ i, TopologicalSpace (π i)]
    (i : ι) (s) : ContinuousOn (fun p : ∀ i, π i => p i) s :=
  Continuous.continuousOn (continuous_apply i)

Continuity of Projection Maps on Product Spaces

Informal description

For any family of topological spaces $\{\pi_i\}_{i \in \iota}$ and any subset $s$ of the product space $\prod_{i \in \iota} \pi_i$, the projection map $p \mapsto p_i$ is continuous on $s$ for each index $i \in \iota$.

continuousOn_const theorem

{s : Set α} {c : β} : ContinuousOn (fun _ => c) s

Full source

@[fun_prop]
theorem continuousOn_const {s : Set α} {c : β} : ContinuousOn (fun _ => c) s :=
  continuous_const.continuousOn

Continuity of Constant Functions on Subsets

Informal description

For any topological spaces $\alpha$ and $\beta$, any subset $s \subseteq \alpha$, and any constant $c \in \beta$, the constant function $f : \alpha \to \beta$ defined by $f(x) = c$ for all $x \in \alpha$ is continuous on $s$.

continuousWithinAt_const theorem

{b : β} {s : Set α} {x : α} : ContinuousWithinAt (fun _ : α => b) s x

Full source

theorem continuousWithinAt_const {b : β} {s : Set α} {x : α} :
    ContinuousWithinAt (fun _ : α => b) s x :=
  continuous_const.continuousWithinAt

Continuity of Constant Functions Within Subsets at Points

Informal description

For any topological spaces $\alpha$ and $\beta$, any constant function $f : \alpha \to \beta$ defined by $f(x) = b$ for some fixed $b \in \beta$ is continuous within any subset $s \subseteq \alpha$ at any point $x \in \alpha$.

continuousOn_id theorem

{s : Set α} : ContinuousOn id s

Full source

theorem continuousOn_id {s : Set α} : ContinuousOn id s :=
  continuous_id.continuousOn

Continuity of Identity Function on Subsets

Informal description

The identity function $\text{id} : \alpha \to \alpha$ is continuous on any subset $s \subseteq \alpha$.

continuousOn_id' theorem

(s : Set α) : ContinuousOn (fun x : α => x) s

Full source

@[fun_prop]
theorem continuousOn_id' (s : Set α) : ContinuousOn (fun x : α => x) s := continuousOn_id

Continuity of the Identity Map on Subsets

Informal description

For any subset $s$ of a topological space $\alpha$, the identity function $x \mapsto x$ is continuous on $s$.

continuousWithinAt_id theorem

{s : Set α} {x : α} : ContinuousWithinAt id s x

Full source

theorem continuousWithinAt_id {s : Set α} {x : α} : ContinuousWithinAt id s x :=
  continuous_id.continuousWithinAt

Continuity of Identity Function Within a Subset at a Point

Informal description

For any subset $s$ of a topological space $\alpha$ and any point $x \in \alpha$, the identity function $\text{id} : \alpha \to \alpha$ is continuous at $x$ within $s$.

ContinuousOn.iterate theorem

{f : α → α} {s : Set α} (hcont : ContinuousOn f s) (hmaps : MapsTo f s s) : ∀ n, ContinuousOn (f^[n]) s

Full source

protected theorem ContinuousOn.iterate {f : α → α} {s : Set α} (hcont : ContinuousOn f s)
    (hmaps : MapsTo f s s) : ∀ n, ContinuousOn (f^[n]) s
  | 0 => continuousOn_id
  | (n + 1) => (hcont.iterate hmaps n).comp hcont hmaps

Continuity of Iterates on Invariant Subsets

Informal description

Let $f : \alpha \to \alpha$ be a function and $s \subseteq \alpha$ a subset. If $f$ is continuous on $s$ and maps $s$ into itself (i.e., $f(s) \subseteq s$), then for any natural number $n$, the $n$-th iterate $f^{[n]}$ is also continuous on $s$.

ContinuousWithinAt.finCons theorem

 {f : α → π 0} {g : α → ∀ j : Fin n, π (Fin.succ j)} {a : α} {s : Set α} (hf : ContinuousWithinAt f s a)
  (hg : ContinuousWithinAt g s a) : ContinuousWithinAt (fun a => Fin.cons (f a) (g a)) s a

Full source

theorem ContinuousWithinAt.finCons
    {f : α → π 0} {g : α → ∀ j : Fin n, π (Fin.succ j)} {a : α} {s : Set α}
    (hf : ContinuousWithinAt f s a) (hg : ContinuousWithinAt g s a) :
    ContinuousWithinAt (fun a => Fin.cons (f a) (g a)) s a :=
  hf.tendsto.finCons hg

Continuity of Fin.cons within a Subset

Informal description

Let $f : \alpha \to \pi(0)$ and $g : \alpha \to \prod_{j \in \text{Fin} n} \pi(\text{Fin.succ} j)$ be functions, and let $a \in \alpha$ be a point in a subset $s \subseteq \alpha$. If $f$ is continuous at $a$ within $s$ and $g$ is continuous at $a$ within $s$, then the function $x \mapsto \text{Fin.cons}(f(x), g(x))$ is also continuous at $a$ within $s$.

ContinuousOn.finCons theorem

 {f : α → π 0} {s : Set α} {g : α → ∀ j : Fin n, π (Fin.succ j)} (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
  ContinuousOn (fun a => Fin.cons (f a) (g a)) s

Full source

theorem ContinuousOn.finCons {f : α → π 0} {s : Set α} {g : α → ∀ j : Fin n, π (Fin.succ j)}
    (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
    ContinuousOn (fun a => Fin.cons (f a) (g a)) s := fun a ha =>
  (hf a ha).finCons (hg a ha)

Continuity of Fin.cons on a Subset

Informal description

Let $f : \alpha \to \pi(0)$ and $g : \alpha \to \prod_{j \in \text{Fin} n} \pi(\text{Fin.succ} j)$ be functions defined on a subset $s \subseteq \alpha$. If $f$ is continuous on $s$ and $g$ is continuous on $s$, then the function $x \mapsto \text{Fin.cons}(f(x), g(x))$ is also continuous on $s$.

ContinuousWithinAt.matrixVecCons theorem

 {f : α → β} {g : α → Fin n → β} {a : α} {s : Set α} (hf : ContinuousWithinAt f s a) (hg : ContinuousWithinAt g s a) :
  ContinuousWithinAt (fun a => Matrix.vecCons (f a) (g a)) s a

Full source

theorem ContinuousWithinAt.matrixVecCons {f : α → β} {g : α → Fin n → β} {a : α} {s : Set α}
    (hf : ContinuousWithinAt f s a) (hg : ContinuousWithinAt g s a) :
    ContinuousWithinAt (fun a => Matrix.vecCons (f a) (g a)) s a :=
  hf.tendsto.matrixVecCons hg

Continuity of Vector Construction within a Subset

Informal description

Let $f : \alpha \to \beta$ and $g : \alpha \to \text{Fin } n \to \beta$ be functions, and let $a \in \alpha$ be a point in a subset $s \subseteq \alpha$. If $f$ is continuous at $a$ within $s$ and $g$ is continuous at $a$ within $s$, then the function $x \mapsto \text{vecCons}(f(x), g(x))$ is continuous at $a$ within $s$.

ContinuousOn.matrixVecCons theorem

 {f : α → β} {g : α → Fin n → β} {s : Set α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
  ContinuousOn (fun a => Matrix.vecCons (f a) (g a)) s

Full source

theorem ContinuousOn.matrixVecCons {f : α → β} {g : α → Fin n → β} {s : Set α}
    (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
    ContinuousOn (fun a => Matrix.vecCons (f a) (g a)) s := fun a ha =>
  (hf a ha).matrixVecCons (hg a ha)

Continuity of Vector Construction on a Subset

Informal description

Let $f : \alpha \to \beta$ and $g : \alpha \to \text{Fin } n \to \beta$ be functions defined on a subset $s \subseteq \alpha$. If $f$ is continuous on $s$ and $g$ is continuous on $s$, then the function $x \mapsto \text{vecCons}(f(x), g(x))$ is also continuous on $s$.

ContinuousWithinAt.finSnoc theorem

 {f : α → ∀ j : Fin n, π (Fin.castSucc j)} {g : α → π (Fin.last _)} {a : α} {s : Set α} (hf : ContinuousWithinAt f s a)
  (hg : ContinuousWithinAt g s a) : ContinuousWithinAt (fun a => Fin.snoc (f a) (g a)) s a

Full source

theorem ContinuousWithinAt.finSnoc
    {f : α → ∀ j : Fin n, π (Fin.castSucc j)} {g : α → π (Fin.last _)} {a : α} {s : Set α}
    (hf : ContinuousWithinAt f s a) (hg : ContinuousWithinAt g s a) :
    ContinuousWithinAt (fun a => Fin.snoc (f a) (g a)) s a :=
  hf.tendsto.finSnoc hg

Continuity of Snoc Operation for Functions Continuous Within a Subset

Informal description

Let $f : \alpha \to \prod_{j\in \text{Fin } n} \pi(\text{castSucc } j)$ and $g : \alpha \to \pi(\text{last } n)$ be functions, and let $a \in \alpha$ be a point in a subset $s \subseteq \alpha$. If $f$ is continuous at $a$ within $s$ and $g$ is continuous at $a$ within $s$, then the function $x \mapsto \text{snoc}(f(x), g(x))$ is continuous at $a$ within $s$.

ContinuousOn.finSnoc theorem

 {f : α → ∀ j : Fin n, π (Fin.castSucc j)} {g : α → π (Fin.last _)} {s : Set α} (hf : ContinuousOn f s)
  (hg : ContinuousOn g s) : ContinuousOn (fun a => Fin.snoc (f a) (g a)) s

Full source

theorem ContinuousOn.finSnoc
    {f : α → ∀ j : Fin n, π (Fin.castSucc j)} {g : α → π (Fin.last _)} {s : Set α}
    (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
    ContinuousOn (fun a => Fin.snoc (f a) (g a)) s := fun a ha =>
  (hf a ha).finSnoc (hg a ha)

Continuity of Snoc Operation for Functions Continuous on a Subset

Informal description

Let $f : \alpha \to \prod_{j\in \text{Fin } n} \pi(\text{castSucc } j)$ and $g : \alpha \to \pi(\text{last } n)$ be functions defined on a subset $s \subseteq \alpha$. If $f$ is continuous on $s$ and $g$ is continuous on $s$, then the function $x \mapsto \text{snoc}(f(x), g(x))$ is continuous on $s$.

ContinuousWithinAt.finInsertNth theorem

 (i : Fin (n + 1)) {f : α → π i} {g : α → ∀ j : Fin n, π (i.succAbove j)} {a : α} {s : Set α}
  (hf : ContinuousWithinAt f s a) (hg : ContinuousWithinAt g s a) :
  ContinuousWithinAt (fun a => i.insertNth (f a) (g a)) s a

Full source

theorem ContinuousWithinAt.finInsertNth
    (i : Fin (n + 1)) {f : α → π i} {g : α → ∀ j : Fin n, π (i.succAbove j)} {a : α} {s : Set α}
    (hf : ContinuousWithinAt f s a) (hg : ContinuousWithinAt g s a) :
    ContinuousWithinAt (fun a => i.insertNth (f a) (g a)) s a :=
  hf.tendsto.finInsertNth i hg

Continuity of Insertion Operation for Functions Continuous Within a Subset

Informal description

Let $i$ be an index in $\text{Fin}(n+1)$, and let $f : \alpha \to \pi_i$ and $g : \alpha \to \prod_{j \in \text{Fin}(n)} \pi_{i.\text{succAbove}\,j}$ be functions. For a point $a \in \alpha$ and a subset $s \subseteq \alpha$, if $f$ is continuous at $a$ within $s$ and $g$ is continuous at $a$ within $s$, then the function $x \mapsto i.\text{insertNth}(f(x), g(x))$ is continuous at $a$ within $s$.

ContinuousOn.finInsertNth theorem

 (i : Fin (n + 1)) {f : α → π i} {g : α → ∀ j : Fin n, π (i.succAbove j)} {s : Set α} (hf : ContinuousOn f s)
  (hg : ContinuousOn g s) : ContinuousOn (fun a => i.insertNth (f a) (g a)) s

Full source

theorem ContinuousOn.finInsertNth
    (i : Fin (n + 1)) {f : α → π i} {g : α → ∀ j : Fin n, π (i.succAbove j)} {s : Set α}
    (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
    ContinuousOn (fun a => i.insertNth (f a) (g a)) s := fun a ha =>
  (hf a ha).finInsertNth i (hg a ha)

Continuity of Insertion Operation for Functions Continuous on a Subset

Informal description

Let $i$ be an index in $\text{Fin}(n+1)$, and let $f : \alpha \to \pi_i$ and $g : \alpha \to \prod_{j \in \text{Fin}(n)} \pi_{i.\text{succAbove}\,j}$ be functions defined on a subset $s \subseteq \alpha$. If $f$ is continuous on $s$ and $g$ is continuous on $s$, then the function $x \mapsto i.\text{insertNth}(f(x), g(x))$ is continuous on $s$.

Set.LeftInvOn.map_nhdsWithin_eq theorem

 {f : α → β} {g : β → α} {x : β} {s : Set β} (h : LeftInvOn f g s) (hx : f (g x) = x)
  (hf : ContinuousWithinAt f (g '' s) (g x)) (hg : ContinuousWithinAt g s x) : map g (𝓝[s] x) = 𝓝[g '' s] g x

Full source

theorem Set.LeftInvOn.map_nhdsWithin_eq {f : α → β} {g : β → α} {x : β} {s : Set β}
    (h : LeftInvOn f g s) (hx : f (g x) = x) (hf : ContinuousWithinAt f (g '' s) (g x))
    (hg : ContinuousWithinAt g s x) : map g (𝓝[s] x) = 𝓝[g '' s] g x := by
  apply le_antisymm
  · exact hg.tendsto_nhdsWithin (mapsTo_image _ _)
  · have A : g ∘ fg ∘ f =ᶠ[𝓝[g '' s] g x] id :=
      h.rightInvOn_image.eqOn.eventuallyEq_of_mem self_mem_nhdsWithin
    refine le_map_of_right_inverse A ?_
    simpa only [hx] using hf.tendsto_nhdsWithin (h.mapsTo (surjOn_image _ _))

Equality of Neighborhood Filters Under Left Inverse Mapping

Informal description

Let $f : \alpha \to \beta$ and $g : \beta \to \alpha$ be functions, $x \in \beta$ a point, and $s \subseteq \beta$ a set. If: 1. $f$ is a left inverse of $g$ on $s$ (i.e., $f(g(y)) = y$ for all $y \in s$), 2. $f(g(x)) = x$, 3. $f$ is continuous within $g(s)$ at $g(x)$, and 4. $g$ is continuous within $s$ at $x$, then the image under $g$ of the neighborhood filter of $x$ within $s$ equals the neighborhood filter of $g(x)$ within $g(s)$. In other words, $g_*(\mathcal{N}_s(x)) = \mathcal{N}_{g(s)}(g(x))$.

Function.LeftInverse.map_nhds_eq theorem

 {f : α → β} {g : β → α} {x : β} (h : Function.LeftInverse f g) (hf : ContinuousWithinAt f (range g) (g x))
  (hg : ContinuousAt g x) : map g (𝓝 x) = 𝓝[range g] g x

Full source

theorem Function.LeftInverse.map_nhds_eq {f : α → β} {g : β → α} {x : β}
    (h : Function.LeftInverse f g) (hf : ContinuousWithinAt f (range g) (g x))
    (hg : ContinuousAt g x) : map g (𝓝 x) = 𝓝[range g] g x := by
  simpa only [nhdsWithin_univ, image_univ] using
    (h.leftInvOn univ).map_nhdsWithin_eq (h x) (by rwa [image_univ]) hg.continuousWithinAt

Equality of Neighborhood Filters under Left Inverse with Continuity Conditions

Informal description

Let $f \colon \alpha \to \beta$ and $g \colon \beta \to \alpha$ be functions between topological spaces, and let $x \in \beta$. If: 1. $f$ is a left inverse of $g$ (i.e., $f(g(y)) = y$ for all $y \in \beta$), 2. $f$ is continuous within the range of $g$ at the point $g(x)$, and 3. $g$ is continuous at $x$, then the image under $g$ of the neighborhood filter of $x$ equals the neighborhood filter of $g(x)$ within the range of $g$. In other words, $g_*(\mathcal{N}(x)) = \mathcal{N}_{\text{range}\,g}(g(x))$.

Topology.IsInducing.continuousWithinAt_iff theorem

 {f : α → β} {g : β → γ} (hg : IsInducing g) {s : Set α} {x : α} :
  ContinuousWithinAt f s x ↔ ContinuousWithinAt (g ∘ f) s x

Full source

lemma Topology.IsInducing.continuousWithinAt_iff {f : α → β} {g : β → γ} (hg : IsInducing g)
    {s : Set α} {x : α} : ContinuousWithinAtContinuousWithinAt f s x ↔ ContinuousWithinAt (g ∘ f) s x := by
  simp_rw [ContinuousWithinAt, hg.tendsto_nhds_iff]; rfl

Characterization of Relative Continuity via Inducing Maps

Informal description

Let $g : \beta \to \gamma$ be an inducing map between topological spaces. For any function $f : \alpha \to \beta$, set $s \subseteq \alpha$, and point $x \in \alpha$, the function $f$ is continuous within $s$ at $x$ if and only if the composition $g \circ f$ is continuous within $s$ at $x$. In other words, $f$ is continuous at $x$ relative to $s$ if and only if $g \circ f$ is continuous at $x$ relative to $s$.

Topology.IsInducing.continuousOn_iff theorem

{f : α → β} {g : β → γ} (hg : IsInducing g) {s : Set α} : ContinuousOn f s ↔ ContinuousOn (g ∘ f) s

Full source

lemma Topology.IsInducing.continuousOn_iff {f : α → β} {g : β → γ} (hg : IsInducing g)
    {s : Set α} : ContinuousOnContinuousOn f s ↔ ContinuousOn (g ∘ f) s := by
  simp_rw [ContinuousOn, hg.continuousWithinAt_iff]

Characterization of Continuity on Subsets via Inducing Maps

Informal description

Let $g : \beta \to \gamma$ be an inducing map between topological spaces. For any function $f : \alpha \to \beta$ and subset $s \subseteq \alpha$, the function $f$ is continuous on $s$ if and only if the composition $g \circ f$ is continuous on $s$.

Topology.IsEmbedding.continuousOn_iff theorem

{f : α → β} {g : β → γ} (hg : IsEmbedding g) {s : Set α} : ContinuousOn f s ↔ ContinuousOn (g ∘ f) s

Full source

lemma Topology.IsEmbedding.continuousOn_iff {f : α → β} {g : β → γ} (hg : IsEmbedding g)
    {s : Set α} : ContinuousOnContinuousOn f s ↔ ContinuousOn (g ∘ f) s :=
  hg.isInducing.continuousOn_iff

Characterization of Continuity on Subsets via Embeddings

Informal description

Let $g \colon \beta \to \gamma$ be an embedding between topological spaces. For any function $f \colon \alpha \to \beta$ and subset $s \subseteq \alpha$, the function $f$ is continuous on $s$ if and only if the composition $g \circ f$ is continuous on $s$.

Topology.IsEmbedding.map_nhdsWithin_eq theorem

{f : α → β} (hf : IsEmbedding f) (s : Set α) (x : α) : map f (𝓝[s] x) = 𝓝[f '' s] f x

Full source

lemma Topology.IsEmbedding.map_nhdsWithin_eq {f : α → β} (hf : IsEmbedding f) (s : Set α) (x : α) :
    map f (𝓝[s] x) = 𝓝[f '' s] f x := by
  rw [nhdsWithin, Filter.map_inf hf.injective, hf.map_nhds_eq, map_principal, ← nhdsWithin_inter',
    inter_eq_self_of_subset_right (image_subset_range _ _)]

Preservation of Neighborhood Filters under Embeddings

Informal description

Let $f \colon \alpha \to \beta$ be an embedding between topological spaces. For any subset $s \subseteq \alpha$ and any point $x \in \alpha$, the image under $f$ of the neighborhood filter of $x$ within $s$ is equal to the neighborhood filter of $f(x)$ within the image $f(s)$, i.e., \[ f_*(\mathcal{N}_s(x)) = \mathcal{N}_{f(s)}(f(x)). \]

Topology.IsOpenEmbedding.map_nhdsWithin_preimage_eq theorem

{f : α → β} (hf : IsOpenEmbedding f) (s : Set β) (x : α) : map f (𝓝[f ⁻¹' s] x) = 𝓝[s] f x

Full source

theorem Topology.IsOpenEmbedding.map_nhdsWithin_preimage_eq {f : α → β} (hf : IsOpenEmbedding f)
    (s : Set β) (x : α) : map f (𝓝[f ⁻¹' s] x) = 𝓝[s] f x := by
  rw [hf.isEmbedding.map_nhdsWithin_eq, image_preimage_eq_inter_range]
  apply nhdsWithin_eq_nhdsWithin (mem_range_self _) hf.isOpen_range
  rw [inter_assoc, inter_self]

Neighborhood Filter Preservation under Open Embedding

Informal description

Let $f \colon \alpha \to \beta$ be an open embedding between topological spaces. For any subset $s \subseteq \beta$ and any point $x \in \alpha$, the image under $f$ of the neighborhood filter of $x$ within the preimage $f^{-1}(s)$ is equal to the neighborhood filter of $f(x)$ within $s$, i.e., \[ f_*(\mathcal{N}_{f^{-1}(s)}(x)) = \mathcal{N}_s(f(x)). \]

Topology.IsQuotientMap.continuousOn_isOpen_iff theorem

 {f : α → β} {g : β → γ} (h : IsQuotientMap f) {s : Set β} (hs : IsOpen s) :
  ContinuousOn g s ↔ ContinuousOn (g ∘ f) (f ⁻¹' s)

Full source

theorem Topology.IsQuotientMap.continuousOn_isOpen_iff {f : α → β} {g : β → γ} (h : IsQuotientMap f)
    {s : Set β} (hs : IsOpen s) : ContinuousOnContinuousOn g s ↔ ContinuousOn (g ∘ f) (f ⁻¹' s) := by
  simp only [continuousOn_iff_continuous_restrict, (h.restrictPreimage_isOpen hs).continuous_iff]
  rfl

Continuity on Open Sets via Quotient Maps

Informal description

Let $f \colon X \to Y$ be a quotient map between topological spaces and $s \subseteq Y$ an open subset. Then a function $g \colon Y \to Z$ is continuous on $s$ if and only if the composition $g \circ f \colon X \to Z$ is continuous on the preimage $f^{-1}(s)$.

IsOpenMap.continuousOn_image_of_leftInvOn theorem

 {f : α → β} {s : Set α} (h : IsOpenMap (s.restrict f)) {finv : β → α} (hleft : LeftInvOn finv f s) :
  ContinuousOn finv (f '' s)

Full source

theorem IsOpenMap.continuousOn_image_of_leftInvOn {f : α → β} {s : Set α}
    (h : IsOpenMap (s.restrict f)) {finv : β → α} (hleft : LeftInvOn finv f s) :
    ContinuousOn finv (f '' s) := by
  refine continuousOn_iff'.2 fun t ht => ⟨f '' (t ∩ s), ?_, ?_⟩
  · rw [← image_restrict]
    exact h _ (ht.preimage continuous_subtype_val)
  · rw [inter_eq_self_of_subset_left (image_subset f inter_subset_right), hleft.image_inter']

Continuity of Left Inverse on Image of Open Map Restriction

Informal description

Let $X$ and $Y$ be topological spaces, $f : X \to Y$ a function defined on a subset $s \subseteq X$, and $f_{inv} : Y \to X$ a left inverse of $f$ on $s$ (i.e., $f_{inv}(f(x)) = x$ for all $x \in s$). If the restriction of $f$ to $s$ is an open map, then $f_{inv}$ is continuous on the image $f(s) \subseteq Y$.

IsOpenMap.continuousOn_range_of_leftInverse theorem

 {f : α → β} (hf : IsOpenMap f) {finv : β → α} (hleft : Function.LeftInverse finv f) : ContinuousOn finv (range f)

Full source

theorem IsOpenMap.continuousOn_range_of_leftInverse {f : α → β} (hf : IsOpenMap f) {finv : β → α}
    (hleft : Function.LeftInverse finv f) : ContinuousOn finv (range f) := by
  rw [← image_univ]
  exact (hf.restrict isOpen_univ).continuousOn_image_of_leftInvOn fun x _ => hleft x

Continuity of Left Inverse on Range of Open Map

Informal description

Let $f \colon X \to Y$ be an open map between topological spaces, and let $f_{inv} \colon Y \to X$ be a left inverse of $f$ (i.e., $f_{inv}(f(x)) = x$ for all $x \in X$). Then $f_{inv}$ is continuous on the range of $f$.

ContinuousOn.union_continuousAt theorem

 {f : α → β} (s_op : IsOpen s) (hs : ContinuousOn f s) (ht : ∀ x ∈ t, ContinuousAt f x) : ContinuousOn f (s ∪ t)

Full source

/-- If `f` is continuous on an open set `s` and continuous at each point of another
set `t` then `f` is continuous on `s ∪ t`. -/
lemma ContinuousOn.union_continuousAt {f : α → β} (s_op : IsOpen s)
    (hs : ContinuousOn f s) (ht : ∀ x ∈ t, ContinuousAt f x) :
    ContinuousOn f (s ∪ t) :=
  continuousOn_of_forall_continuousAt <| fun _ hx => hx.elim
  (fun h => ContinuousWithinAt.continuousAt (continuousWithinAt hs h) <| IsOpen.mem_nhds s_op h)
  (ht _)

Continuity on Union of Open Set and Pointwise Continuous Set

Informal description

Let $f \colon \alpha \to \beta$ be a function between topological spaces, $s \subseteq \alpha$ an open subset, and $t \subseteq \alpha$ an arbitrary subset. If $f$ is continuous on $s$ and continuous at every point of $t$, then $f$ is continuous on $s \cup t$.

ContinuousOn.union_isClosed theorem

 (hs : IsClosed s) (ht : IsClosed t) {f : α → β} (hfs : ContinuousOn f s) (hft : ContinuousOn f t) :
  ContinuousOn f (s ∪ t)

Full source

/-- If a function is continuous on two closed sets, it is also continuous on their union. -/
theorem ContinuousOn.union_isClosed (hs : IsClosed s)
    (ht : IsClosed t) {f : α → β} (hfs : ContinuousOn f s)
    (hft : ContinuousOn f t) : ContinuousOn f (s ∪ t) := by
  refine fun x hx ↦ .union ?_ ?_
  · refine if hx : x ∈ s then hfs x hx else continuousWithinAt_of_not_mem_closure ?_
    rwa [hs.closure_eq]
  · refine if hx : x ∈ t then hft x hx else continuousWithinAt_of_not_mem_closure ?_
    rwa [ht.closure_eq]

Continuity on Union of Closed Sets

Informal description

Let $s$ and $t$ be closed subsets of a topological space $\alpha$, and let $f : \alpha \to \beta$ be a function that is continuous on both $s$ and $t$. Then $f$ is continuous on the union $s \cup t$.

ContinuousOn.tendsto_nhdsSet theorem

 {f : α → β} {s s' : Set α} {t : Set β} (hf : ContinuousOn f s') (hs' : s' ∈ 𝓝ˢ s) (hst : MapsTo f s t) :
  Tendsto f (𝓝ˢ s) (𝓝ˢ t)

Full source

/-- If `f` is continuous on some neighbourhood `s'` of `s` and `f` maps `s` to `t`,
the preimage of a set neighbourhood of `t` is a set neighbourhood of `s`. -/
-- See `Continuous.tendsto_nhdsSet` for a special case.
theorem ContinuousOn.tendsto_nhdsSet {f : α → β} {s s' : Set α} {t : Set β}
    (hf : ContinuousOn f s') (hs' : s' ∈ 𝓝ˢ s) (hst : MapsTo f s t) : Tendsto f (𝓝ˢ s) (𝓝ˢ t) := by
  obtain ⟨V, hV, hsV, hVs'⟩ := mem_nhdsSet_iff_exists.mp hs'
  refine ((hasBasis_nhdsSet s).tendsto_iff (hasBasis_nhdsSet t)).mpr fun U hU ↦
    ⟨V ∩ f ⁻¹' U, ?_, fun _ ↦ ?_⟩
  · exact ⟨(hf.mono hVs').isOpen_inter_preimage hV hU.1,
      subset_inter hsV (hst.mono Subset.rfl hU.2)⟩
  · intro h
    rw [← mem_preimage]
    exact mem_of_mem_inter_right h

Continuity on Neighborhood Implies Filter Continuity

Informal description

Let $X$ and $Y$ be topological spaces, $f : X \to Y$ a function, and $s, s' \subseteq X$, $t \subseteq Y$ subsets. If $f$ is continuous on $s'$, $s'$ is a neighborhood of $s$ (i.e., $s' \in \mathcal{N}(s)$), and $f$ maps $s$ into $t$, then $f$ maps the neighborhood filter of $s$ to the neighborhood filter of $t$. In other words, $f$ induces a continuous map at the level of neighborhood filters: $\mathcal{N}(s) \to \mathcal{N}(t)$.

Continuous.tendsto_nhdsSet theorem

{f : α → β} {t : Set β} (hf : Continuous f) (hst : MapsTo f s t) : Tendsto f (𝓝ˢ s) (𝓝ˢ t)

Full source

/-- Preimage of a set neighborhood of `t` under a continuous map `f` is a set neighborhood of `s`
provided that `f` maps `s` to `t`. -/
theorem Continuous.tendsto_nhdsSet {f : α → β} {t : Set β} (hf : Continuous f)
    (hst : MapsTo f s t) : Tendsto f (𝓝ˢ s) (𝓝ˢ t) :=
  hf.continuousOn.tendsto_nhdsSet univ_mem hst

Continuous Function Maps Neighborhood Filters to Neighborhood Filters

Informal description

Let $X$ and $Y$ be topological spaces, $f \colon X \to Y$ a continuous function, and $s \subseteq X$, $t \subseteq Y$ subsets. If $f$ maps $s$ into $t$, then $f$ maps the neighborhood filter of $s$ to the neighborhood filter of $t$. In other words, $f$ induces a continuous map at the level of neighborhood filters: $\mathcal{N}(s) \to \mathcal{N}(t)$.

Continuous.tendsto_nhdsSet_nhds theorem

{b : β} {f : α → β} (h : Continuous f) (h' : EqOn f (fun _ ↦ b) s) : Tendsto f (𝓝ˢ s) (𝓝 b)

Full source

lemma Continuous.tendsto_nhdsSet_nhds
    {b : β} {f : α → β} (h : Continuous f) (h' : EqOn f (fun _ ↦ b) s) :
    Tendsto f (𝓝ˢ s) (𝓝 b) := by
  rw [← nhdsSet_singleton]
  exact h.tendsto_nhdsSet h'

Continuous Function Maps Neighborhood Filter of Set to Point Neighborhood Filter When Constant on Set

Informal description

Let $X$ and $Y$ be topological spaces, $f \colon X \to Y$ a continuous function, $s \subseteq X$ a subset, and $b \in Y$ a point. If $f$ is constant and equal to $b$ on $s$, then $f$ maps the neighborhood filter of $s$ to the neighborhood filter of $b$. In other words, $f$ induces a continuous map at the level of neighborhood filters: $\mathcal{N}(s) \to \mathcal{N}(b)$.

Notation