tendsto_extendFrom
theorem tendsto_extendFrom :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {A : Set X} {f : X → Y}
{x : X},
(∃ y, Filter.Tendsto f (nhdsWithin x A) (nhds y)) → Filter.Tendsto f (nhdsWithin x A) (nhds (extendFrom A f x))
The theorem `tendsto_extendFrom` states that if a function `f` from a set `A` has a limit `y` as `x` tends towards `x₀` within `A`, then the function `f` will tend towards the value given by extending the function from `A` at `x₀`, as `x` tends towards `x₀` within `A`. In other words, if there exists a `y` such that `f` converges to `y` when `x` approaches `x₀` within `A`, then `f` also converges to the extended version of `f` at `x₀` when `x` approaches `x₀` within `A`. This theorem encapsulates the idea that the limit of a function over a subset of its domain can be extended to the entire domain.
More concisely: If a function `f` has a limit `y` as `x` approaches `x₀` in a set `A`, then `f` also has the limit `y` at `x₀` when extended to `x₀` within `A`.
|
continuousOn_extendFrom
theorem continuousOn_extendFrom :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : RegularSpace Y]
{f : X → Y} {A B : Set X},
B ⊆ closure A → (∀ x ∈ B, ∃ y, Filter.Tendsto f (nhdsWithin x A) (nhds y)) → ContinuousOn (extendFrom A f) B
The theorem `continuousOn_extendFrom` states that given any two sets `A` and `B` in a topological space `X` and a function `f` from `X` to a T₃ space `Y` such that every point in `B` is a limit point of `A` (i.e., `B` is a subset of the closure of `A`), if the function `f` has a limit within `A` at every point of `B`, then the extension of the function `f` from the set `A` is continuous on `B`. Here, the extension of `f` from `A` is defined as a function that at any point `x₀`, takes the limit value of `f` as `x` tends to `x₀` within `A`, if such a limit exists.
More concisely: If a function from a topological space to a T₃ space is limit continuous at all limit points of a set in its domain, then its extension to the set is continuous.
|
extendFrom_eq
theorem extendFrom_eq :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : T2Space Y]
{A : Set X} {f : X → Y} {x : X} {y : Y},
x ∈ closure A → Filter.Tendsto f (nhdsWithin x A) (nhds y) → extendFrom A f x = y
The theorem `extendFrom_eq` states that for any types `X` and `Y` endowed with topological space structures (where `Y` is also a T2 space, also known as a Hausdorff space), given a set `A` of `X`, a function `f` from `X` to `Y`, and elements `x` of `X` and `y` of `Y`, if `x` belongs to the closure of set `A` and the function `f` tends to `y` at `x` within the set `A` (as formalized by the `Filter.Tendsto` predicate), then the function `extendFrom A f`, which extends the function `f` from the set `A`, evaluates to `y` at `x`. In other words, the extended function at `x` is the limit of the original function `f` as we approach `x` within the set `A`, if such a limit exists at `y`.
More concisely: If a function `f` from a set `A` in a T2 topological space `X` to a topological space `Y`, with closure `cl(A)`, tends to `y` at every limit point `x` in `cl(A)`, then `extendFrom A f` evaluates to `y` at `x`.
|
continuous_extendFrom
theorem continuous_extendFrom :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : RegularSpace Y]
{f : X → Y} {A : Set X},
Dense A → (∀ (x : X), ∃ y, Filter.Tendsto f (nhdsWithin x A) (nhds y)) → Continuous (extendFrom A f)
The theorem `continuous_extendFrom` states that if we have a function `f` from a type `X` to a T₃ space `Y`, and a dense set `A` of `X`, such that for every `x` in `X`, the function `f` has a limit within `A`, then the function that extends `f` from `A` is a continuous function. In other words, if `f` approaches some limit as `x` approaches any point in the set `A` (which is dense in the topological space `X`), then the function that extends `f` from `A` is continuous in the topological sense, i.e., it preserves the topological structure of the space.
More concisely: If `f` is a function from a dense subset `A` of the topological space `X` to a T₃ space `Y` such that `f` has a limit at every point in `A`, then the continuous extension of `f` from `A` to all of `X` is itself a continuous function.
|