continuousOn_const
theorem continuousOn_const :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set α} {c : β},
ContinuousOn (fun x => c) s
This theorem states that for any types `α` and `β` which have topological space structures, any set `s` of the type `α`, and any element `c` of the type `β`, the function that maps every element of `s` to `c` is continuous on `s`. In other words, a constant function is always continuous on any set within the corresponding topological spaces.
More concisely: For any topological spaces `α` and `β`, and any set `s` in `α` and constant function `f : s -> β` with image `{f(x) | x ∈ s} = {c}`, the function `f` is continuous on `s`.
|
continuous_piecewise
theorem continuous_piecewise :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set α} {f g : α → β}
[inst_2 : (a : α) → Decidable (a ∈ s)],
(∀ a ∈ frontier s, f a = g a) →
ContinuousOn f (closure s) → ContinuousOn g (closure sᶜ) → Continuous (s.piecewise f g)
This theorem, `continuous_piecewise`, states that for any types `α` and `β`, assumed to be topological spaces, and for a set `s` of type `α`, and two functions `f` and `g` mapping `α` to `β`. Assuming that we can decide for each element of `α` whether it belongs to `s` or not, if for every element on the frontier of `s`, `f` and `g` coincide, and `f` is continuous over the closure of `s`, and `g` is continuous over the closure of the complement of `s`, then the piecewise function that equals `f` on `s` and `g` on its complement is continuous. In simpler words, this theorem guarantees the continuity of a piecewise function under certain conditions about the continuity of its component functions and their agreement on the border of the regions where they are defined.
More concisely: Given topological spaces α and β, sets s ⊆ α, and continuous functions f : α → β and g : α → β with f restriction to s = g restriction to s on the frontier of s, if f is continuous over the closure of s and g is continuous over the closure of s∖s, then the piecewise function (x : α) → if x ∈ s then f x else g x is continuous.
|
eventually_nhdsWithin_of_forall
theorem eventually_nhdsWithin_of_forall :
∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {a : α} {p : α → Prop},
(∀ x ∈ s, p x) → ∀ᶠ (x : α) in nhdsWithin a s, p x
This theorem states that for any type `α` equipped with a topology (a `TopologicalSpace α`), any subset `s` of `α`, any point `a` in `α`, and any property `p` that the elements of `α` may or may not satisfy, if every element in subset `s` satisfies the property `p`, then eventually, every point `x` in the neighborhood within `s` of point `a` also satisfies property `p`. In other words, the property `p` holds true for all points in an arbitrary close neighborhood of `a`, if it holds true for all points in `s`. This theorem is a statement about the "local" behavior of the property `p` at point `a` within the given set `s`.
More concisely: Given a topological space `(α, top)`, a subset `s ⊆ α`, a point `a ∈ α`, and a property `p(x) : Prop`, if `∀ x ∈ s, p(x)` holds, then for every neighborhood `U` of `a` in `s`, `∀ x ∈ U, p(x)` also holds.
|
ContinuousWithinAt.congr
theorem ContinuousWithinAt.congr :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f f₁ : α → β} {s : Set α}
{x : α}, ContinuousWithinAt f s x → (∀ y ∈ s, f₁ y = f y) → f₁ x = f x → ContinuousWithinAt f₁ s x
The theorem `ContinuousWithinAt.congr` states that for any types `α` and `β` equipped with topological structures, given two functions `f` and `f₁` from `α` to `β`, a subset `s` of `α` and a point `x` in `α`, if `f` is continuous at `x` within the subset `s` and `f₁` equals `f` for every point in `s` (i.e., `f₁ y = f y` for all `y` in `s`) and also at the point `x`, then `f₁` is also continuous at `x` within the subset `s`. In other words, the continuity of a function at a point within a subset is preserved under a pointwise equivalent function on that subset.
More concisely: If a function is continuous at a point in a subset and pointwise equal to another function on that subset, then the second function is also continuous at that point in the subset.
|
continuousWithinAt_univ
theorem continuousWithinAt_univ :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (x : α),
ContinuousWithinAt f Set.univ x ↔ ContinuousAt f x
This theorem states that for all types `α` and `β` with topological space structures, for any function `f` from `α` to `β` and for any point `x` in `α`, the function `f` is continuous at `x` within the universal set (which contains all elements of `α`) if and only if `f` is continuous at `x`. In other words, imposing the condition that the continuity of the function is restricted within the universal set doesn't change the fact that the function is continuous at a point.
More concisely: For any types `α` and `β` with topological spaces structures, and for any function `f` from `α` to `β` and point `x` in `α`, the function `f` is continuous at `x` in the universal set if and only if it is continuous at `x` in the pointwise sense.
|
ContinuousWithinAt.congr_of_eventuallyEq
theorem ContinuousWithinAt.congr_of_eventuallyEq :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f f₁ : α → β} {s : Set α}
{x : α}, ContinuousWithinAt f s x → (nhdsWithin x s).EventuallyEq f₁ f → f₁ x = f x → ContinuousWithinAt f₁ s x
This theorem states that for any two functions `f` and `f₁` from a topological space `α` to another topological space `β`, a set `s` of elements from `α`, and a point `x` in `α`, if `f` is continuous at point `x` within the set `s`, and `f₁` equals `f` in a neighborhood within `s` around `x` (i.e., `f₁` and `f` are eventually equal in the neighborhood filter within `s` at `x`), and `f₁` at `x` equals `f` at `x`, then `f₁` is also continuous at point `x` within the set `s`. In other words, continuity of a function at a point within a set is preserved under an eventual equality in a neighborhood around that point.
More concisely: If a function `f:` α -> β is continuous at a point `x` in a set `s` ⊆ α and `f₁:` α -> β equals `f` in a neighborhood of `x` in `s` and `f₁(x) = f(x)`, then `f₁` is continuous at `x` in `s`.
|
self_mem_nhdsWithin
theorem self_mem_nhdsWithin : ∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} {s : Set α}, s ∈ nhdsWithin a s := by
sorry
The theorem `self_mem_nhdsWithin` states that for any given type `α` equipped with a topology, an element `a` of type `α`, and a set `s` of type `α`, the set `s` is an element of the "neighborhood within" filter created from `a` and `s`. In other words, `s` itself is considered a "neighborhood within" `s` of `a` in the given topological space. This implies that `s` contains the intersection of `s` and some neighborhood of `a`.
More concisely: For any topological space $(X, \tau)$, element $a \in X$, and set $s \subseteq X$, we have $s \in \mathit{nhdsWithin} \ a$ (the neighborhood filter of $a$ in $X$), hence $s \cap \mathit{open}(a) \neq \emptyset$.
|
ContinuousWithinAt.insert_self
theorem ContinuousWithinAt.insert_self :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {x : α}
{s : Set α}, ContinuousWithinAt f s x → ContinuousWithinAt f (insert x s) x
This theorem, known as an alias of the reverse direction of `continuousWithinAt_insert_self`, states that for any two topological spaces `α` and `β`, a function `f` from `α` to `β`, a point `x` in `α`, and a set `s` in `α`, if `f` is continuous at point `x` within set `s`, then `f` is also continuous at point `x` within the set formed by inserting `x` into `s`. In mathematical terms, the continuity of `f` at a point `x` within a set `s` implies its continuity at the same point within the set `s ∪ {x}`.
More concisely: If a function `f` is continuous at point `x` within set `s` in topological spaces `α` and `β`, then `f` is continuous at point `x` within the set `s ∪ {x}`.
|
ContinuousAt.continuousOn
theorem ContinuousAt.continuousOn :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α},
(∀ x ∈ s, ContinuousAt f x) → ContinuousOn f s
This theorem states that for any two types `α` and `β`, with both being topological spaces, any function `f` from `α` to `β`, and any set `s` of `α`, if `f` is continuous at every point `x` in `s`, then `f` is continuous on the set `s`. In more mathematical terms, it says that if for each `x` in `s`, the image under `f` of points in `α` arbitrarily close to `x` becomes arbitrarily close to `f(x)`, then for every `x` in `s`, the restriction of `f` to `s` is continuous at `x` within `s`.
More concisely: If `f` is a continuous function from topological space `α` to topological space `β`, and `f` is continuous at every point in a subset `s` of `α`, then `f` is continuous on `s`.
|
continuousOn_pi
theorem continuousOn_pi :
∀ {α : Type u_1} [inst : TopologicalSpace α] {ι : Type u_5} {π : ι → Type u_6}
[inst_1 : (i : ι) → TopologicalSpace (π i)] {f : α → (i : ι) → π i} {s : Set α},
ContinuousOn f s ↔ ∀ (i : ι), ContinuousOn (fun y => f y i) s
This theorem, named `continuousOn_pi`, is about the continuity of functions in topological spaces. It states that for any type `α` with a topological space structure, any type `ι`, a function `π` from `ι` to another type, a function `f` from `α` to the output of `π`, and a set `s` of type `α`, `f` is continuous on the set `s` if and only if, for every element `i` from `ι`, the function that takes an element `y` and maps it to the `i`-th component of `f(y)` is also continuous on `s`. In other words, a function is continuous on a set if and only if it is continuous on that set when evaluated at each component.
More concisely: A function from a topological space to another space is continuous on a set if and only if the projection of its values to each component is continuous on that set.
|
ContinuousWithinAt.comp
theorem ContinuousWithinAt.comp :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
[inst_2 : TopologicalSpace γ] {g : β → γ} {f : α → β} {s : Set α} {t : Set β} {x : α},
ContinuousWithinAt g t (f x) → ContinuousWithinAt f s x → Set.MapsTo f s t → ContinuousWithinAt (g ∘ f) s x
The theorem `ContinuousWithinAt.comp` states that for any three topological spaces `α`, `β`, and `γ`, given two functions `f` from `α` to `β` and `g` from `β` to `γ`, along with subsets `s` of `α` and `t` of `β`, and a point `x` in `α`, if `g` is continuous at the point `f(x)` within `t`, `f` is continuous at `x` within `s`, and `f` maps every point of `s` into `t`, then the composition `g ∘ f` is also continuous at `x` within `s`.
This theorem is a generalization of the standard result in topology that the composition of two continuous functions is continuous. Here, however, the continuity of each function is considered within a particular subset of its domain, and the theorem imposes the additional condition that `f` must map `s` into `t`.
More concisely: Given topological spaces α, β, and γ, functions f : α → β and g : β → γ, subsets s ⊆ α and t ⊆ β, and a point x ∈ α, if g is continuous at f(x) within t, f is continuous at x within s, and f(s) ∋ t, then g ∘ f is continuous at x within s.
|
continuousOn_congr
theorem continuousOn_congr :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → β} {s : Set α},
Set.EqOn g f s → (ContinuousOn g s ↔ ContinuousOn f s)
This theorem, `continuousOn_congr`, states that for any two functions `f` and `g` from a type `α` to a type `β`, both of which are equipped with a topological space structure, and for any set `s` of type `α`, if `g` and `f` are equal on the set `s` (meaning that for every element `x` in `s`, `g(x) = f(x)`), then `g` is continuous on `s` if and only if `f` is continuous on `s`. In mathematical terms, if two functions are equal on a subset of their domain, their continuity on that subset is equivalent.
More concisely: For functions `f` and `g` from a topological space `α` to a topological space `β`, if `g = f` on a subset `s` of `α` and `f` is continuous on `s`, then `g` is also continuous on `s`.
|
continuousOn_id
theorem continuousOn_id : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α}, ContinuousOn id s
This theorem, `continuousOn_id`, states that for any type `α` which has a topological space structure, and for any set `s` of type `α`, the identity function is continuous on `s`. In other words, for each point in the set `s`, the map that takes each point to itself preserves the topological space structure, i.e., the preimage of any open set is also open.
More concisely: For any topological space `(α, τ)` and subset `s ∈ α`, the identity function `id : α → α` is continuous on `s`, meaning the preimage of any open set in `α` under `id` is open in `s`.
|
ContinuousAt.continuousWithinAt
theorem ContinuousAt.continuousWithinAt :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
{x : α}, ContinuousAt f x → ContinuousWithinAt f s x
This theorem states that for any given types `α` and `β`, two topological spaces `α` and `β`, a function `f` from `α` to `β`, a set `s` of `α` and a point `x` of `α`, if the function `f` is continuous at the point `x`, then the function `f` is also continuous at the point `x` within the set `s`. In other words, if the function values approach `f(x)` as the function argument approaches `x` in the whole space, they also approach `f(x)` as the argument approaches `x` while remaining within the subset `s` of the space.
More concisely: If `f` is a continuous function from topological spaces `α` to `β` and `x` is a point in `α` where `f` is continuous, then `f` is continuous at `x` within any subset `s` of `α`.
|
continuousOn_fst
theorem continuousOn_fst :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set (α × β)},
ContinuousOn Prod.fst s
This theorem states that for any types `α` and `β` that have a topological structure (represented by `TopologicalSpace α` and `TopologicalSpace β` instances), and for any set `s` of pairs of elements from `α` and `β` (expressed as `Set (α × β)`), the first projection function (`Prod.fst`) is continuous on this set. In terms of topology, the first projection function, which picks out the first element of each pair in the set `s`, maintains the continuity property; that is, for every point in the set `s`, the function is continuous at that point within the set.
More concisely: For any topological spaces `α` and `β` and a set `s` of pairs from `α × β`, the first projection function `Prod.fst` is continuous on `s`.
|
eventually_nhdsWithin_iff
theorem eventually_nhdsWithin_iff :
∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} {s : Set α} {p : α → Prop},
(∀ᶠ (x : α) in nhdsWithin a s, p x) ↔ ∀ᶠ (x : α) in nhds a, x ∈ s → p x
This theorem states that for any topological space `α`, any point `a` in `α`, any set `s` in `α`, and any property `p` mapped from `α`, the statement "eventually in the neighborhood within `s` at `a`, `p` holds for `x`" is equivalent to the statement "eventually in the neighborhood at `a`, if `x` is in `s` then `p` holds for `x`". Here, "eventually" is used in the sense of filters, meaning that the property holds in some neighborhood of `a`. In other words, the property `p` holds at `a` in the intersection of `s` and some open set around `a` if and only if `p` holds at `a` in `s` for some open set around `a`.
More concisely: For any topological space `α`, point `a` in `α`, set `s` in `α`, and property `p`: the property "eventually in the neighborhood of `a`, `x` in `s` implies `p(x)` holds" is equivalent to "eventually in the neighborhood of `a`, `p` holds at intersecting open sets containing `a` and `s`."
|
continuousOn_iff_continuous_restrict
theorem continuousOn_iff_continuous_restrict :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α},
ContinuousOn f s ↔ Continuous (s.restrict f)
The theorem `continuousOn_iff_continuous_restrict` asserts that for any type `α` and `β` which have a topology, any function `f` from `α` to `β`, and any set `s` of type `α`, the function `f` is continuous on the set `s` if and only if when the function `f` is restricted to the set `s`, it is continuous. In other words, it establishes an equivalence between the continuity of a function on a subset of its domain and the continuity of its restriction to that subset.
More concisely: A function between topological spaces is continuous on a subset if and only if its restriction to that subset is continuous.
|
ContinuousWithinAt.tendsto
theorem ContinuousWithinAt.tendsto :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
{x : α}, ContinuousWithinAt f s x → Filter.Tendsto f (nhdsWithin x s) (nhds (f x))
This theorem states that if a function is continuous within a set `s` at a point `x`, then the function `f` tends to `f(x)` within the set `s` as `x` approaches `x`. This is registered for use with the dot notation, particularly for using `Filter.Tendsto.comp`. Notably, `ContinuousWithinAt.comp` will have a distinct meaning. The theorem is defined for any types `α` and `β` that come equipped with topological spaces, a function `f` from `α` to `β`, a set `s` of `α`, and a point `x` of `α`.
More concisely: If a function `f` is continuous at `x` in set `s`, then `f` converges to `f(x)` as `x` approaches any point in `s`.
|
Embedding.map_nhdsWithin_eq
theorem Embedding.map_nhdsWithin_eq :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
Embedding f → ∀ (s : Set α) (x : α), Filter.map f (nhdsWithin x s) = nhdsWithin (f x) (f '' s)
This theorem states that for any two types `α` and `β`, each equipped with a topological space structure, and any function `f` from `α` to `β` that is an embedding, the image under `f` of the "neighborhood within" filter at a point `x` in a set `s` in `α` is equal to the "neighborhood within" filter at the image of `x` under `f` in the image of `s` under `f`. In mathematical terms, this can be expressed as: for a topological embedding `f : α → β`, the forward map of the filter `nhdsWithin x s` under `f` is equal to `nhdsWithin (f x) (f '' s)`, where `nhdsWithin x s` represents the intersection of a neighborhood of `x` with the set `s`, and `f '' s` is the image of `s` under the function `f`.
More concisely: For a topological embedding `f : α → β`, the image under `f` of the neighborhood filter of a point `x` in a set `s` in `α` is equal to the neighborhood filter of the image of `x` in the image of `s` under `f`.
|
ContinuousOn.mono_rng
theorem ContinuousOn.mono_rng :
∀ {α : Type u_5} {β : Type u_6} {t₁ : TopologicalSpace α} {t₂ t₃ : TopologicalSpace β},
t₂ ≤ t₃ → ∀ {s : Set α} {f : α → β}, ContinuousOn f s → ContinuousOn f s
This theorem states that if a function is continuous on a certain set within a given pair of topologies, then it remains continuous on the same set when we consider a coarser (or equally fine) topology on the target space. In other words, if we have a topological space with two topologies `t₂` and `t₃` on the target space such that `t₂` is finer than or equal to `t₃`, and a function `f` from a set `s` in the source space to the target space is continuous with respect to these topologies, then the function `f` will also be continuous with respect to the coarser topology `t₃` on the set `s`.
More concisely: If a function is continuous on a set with respect to a finer topology on the target space, then it remains continuous on that set with respect to a coarser topology on the target space.
|
Continuous.comp_continuousOn
theorem Continuous.comp_continuousOn :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
[inst_2 : TopologicalSpace γ] {g : β → γ} {f : α → β} {s : Set α},
Continuous g → ContinuousOn f s → ContinuousOn (g ∘ f) s
The theorem `Continuous.comp_continuousOn` states that for any three topological spaces `α`, `β`, and `γ`, if a function `g` from `β` to `γ` is continuous, and a function `f` from `α` to `β` is continuous on a set `s` in `α`, then the composition of `g` and `f` (denoted as `g ∘ f`) is also continuous on the set `s`. In other words, the continuity of the individual functions ensures the continuity of their composition on the specified set.
More concisely: If a function from `α` to `β` is continuous on a set `s` in `α`, and a function from `β` to `γ` is continuous, then their composition is continuous on `s`.
|
ContinuousOn.prod_map
theorem ContinuousOn.prod_map :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : TopologicalSpace α]
[inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] [inst_3 : TopologicalSpace δ] {f : α → γ} {g : β → δ}
{s : Set α} {t : Set β}, ContinuousOn f s → ContinuousOn g t → ContinuousOn (Prod.map f g) (s ×ˢ t)
The theorem `ContinuousOn.prod_map` states that for any two types `α`, `β`, `γ`, and `δ` equipped with topological structures, and any two functions `f : α → γ` and `g : β → δ`, if `f` is continuous on a subset `s` of `α` and `g` is continuous on a subset `t` of `β`, then, the function `Prod.map f g`, which applies `f` and `g` to the respective components of a pair, is continuous on the product set `s ×ˢ t`. This means that the continuity of the functions on their respective domain sets ensures the continuity of the combined function on the cartesian product of the domain sets.
More concisely: If functions `f : α → γ` and `g : β → δ` are continuous on subsets `s ≤ α` and `t ≤ β`, respectively, then the function `Prod.map f g` is continuous on the product set `s × t`.
|
inter_mem_nhdsWithin
theorem inter_mem_nhdsWithin :
∀ {α : Type u_1} [inst : TopologicalSpace α] (s : Set α) {t : Set α} {a : α}, t ∈ nhds a → s ∩ t ∈ nhdsWithin a s
The theorem `inter_mem_nhdsWithin` states that for any type `α` which has a topological space structure, any set `s` of type `α`, any other set `t` of type `α`, and any element `a` of type `α`, if `t` is a neighborhood of `a` (i.e., `t` is in the neighborhood filter of `a`), then the intersection of `s` and `t` is in the "neighborhood within" filter of `a` with respect to `s`. In other words, any intersection of `s` and a neighborhood of `a` is a set containing the intersection of `s` and a neighborhood of `a`. This theorem is a fundamental property in topology, describing how the intersection of sets interacts with the concepts of neighborhood and "neighborhood within" in a topological space.
More concisely: For any topological space `(α, τ)`, if `t ∈ 𝓝(a)` (neighborhood of `a`), then `s ∩ t ∈ 𝓛[s](a)` (intersection of `s` and `t` is in the "neighborhood within" `s` of `a`).
|
Set.LeftInvOn.map_nhdsWithin_eq
theorem Set.LeftInvOn.map_nhdsWithin_eq :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {g : β → α}
{x : β} {s : Set β},
Set.LeftInvOn f g s →
f (g x) = x →
ContinuousWithinAt f (g '' s) (g x) →
ContinuousWithinAt g s x → Filter.map g (nhdsWithin x s) = nhdsWithin (g x) (g '' s)
The theorem `Set.LeftInvOn.map_nhdsWithin_eq` states that for any types `α` and `β` that are topological spaces, given two functions `f : α → β` and `g : β → α`, a point `x` of type `β`, and a set `s` of type `β`, if `f` is a left inverse to `g` on `s`, `f (g x)` equals `x`, `f` is continuous at `g x` within the image of `s` under `g`, and `g` is continuous at `x` within `s`, then the forward map of the "neighbourhood within" filter of `x` in `s` under `g` equals the "neighbourhood within" filter of `g x` in the image of `s` under `g`. In simpler terms, it says that if `f` and `g` satisfy certain conditions relating to continuity and being inverses, then applying `g` to the "close" elements to `x` in `s` gives the same result as looking at the "close" elements to `g x` in the image of `s` under `g`.
More concisely: If functions `f : α → β` and `g : β → α` satisfy `f ∘ g = id_β` on a set `s ⊆ β`, `f` is continuous at `g x` in the image of `s` under `g`, and `g` is continuous at `x` in `s`, then the forward image of the neighborhood filter of `x` in `s` under `g` equals the neighborhood filter of `g x` in the image of `s` under `g`.
|
nhdsWithin_le_iff
theorem nhdsWithin_le_iff :
∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : Set α} {x : α},
nhdsWithin x s ≤ nhdsWithin x t ↔ t ∈ nhdsWithin x s
This theorem states that for any type `α` equipped with a topology (i.e., a `TopologicalSpace α`), for any two sets `s` and `t` of type `α`, and for any element `x` of type `α`, the "neighborhood within" `s` of `x` is less than or equal to the "neighborhood within" `t` of `x` if and only if `t` is in the "neighborhood within" `s` of `x`.
In more mathematically precise terms: given a topological space $(\alpha, \tau)$, two subsets $s, t \subset \alpha$, and a point $x \in \alpha$, the filter generated by the intersection of `s` and a neighborhood of `x` is a subset of the filter generated by the intersection of `t` and a neighborhood of `x` if and only if `t` is an element of the filter generated by the intersection of `s` and a neighborhood of `x`.
More concisely: For any topological space $(\alpha, \tau)$, and for any sets $s, t \subseteq \alpha$ and point $x \in \alpha$, the filter generated by $s \cap N$ contains the filter generated by $t \cap N$ if and only if $t \in s \cap N$, where $N$ is a neighborhood of $x$.
|
nhdsWithin_restrict''
theorem nhdsWithin_restrict'' :
∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} (s : Set α) {t : Set α},
t ∈ nhdsWithin a s → nhdsWithin a s = nhdsWithin a (s ∩ t)
This theorem states that for any type `α` with a topological space structure, any element `a` of type `α`, and any sets `s` and `t` of type `α`, if `t` is in the neighborhood within `s` of `a`, then the neighborhood within `s` of `a` is equivalent to the neighborhood within the intersection of `s` and `t` of `a`. In simpler terms, if `t` is a neighborhood of `a` within `s`, then the neighborhoods of `a` within `s` are the same as the neighborhoods of `a` within the intersection of `s` and `t`.
More concisely: For any topological space `α` and elements `a` in `α`, sets `s` and `t` in `α` such that `t` is a neighborhood of `a` in `s`, the neighborhood filter of `a` in `s` is equal to the neighborhood filter of `a` in the intersection of `s` and `t`.
|
nhdsWithin_singleton
theorem nhdsWithin_singleton : ∀ {α : Type u_1} [inst : TopologicalSpace α] (a : α), nhdsWithin a {a} = pure a := by
sorry
The theorem `nhdsWithin_singleton` states that for any type `α` equipped with a topological space structure and for any element `a` of `α`, the neighborhood within the singleton set `{a}` of `a` is equal to `pure a`. In other words, the filter that captures the notion of "being close to `a` within `{a}`" in `α` is just the filter that isolates `a` itself.
More concisely: For any topological space `(α, τ)`, the neighborhood filter of `a` in the singleton set `{a} ⊆ α` equals the principal filter generated by `a`, i.e., `{U ∈ τ | a ∈ U} = ∇{a}`.
|
continuous_prod_of_discrete_left
theorem continuous_prod_of_discrete_left :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
[inst_2 : TopologicalSpace γ] [inst_3 : DiscreteTopology α] {f : α × β → γ},
Continuous f ↔ ∀ (a : α), Continuous fun x => f (a, x)
This theorem states that for three types `α`, `β`, and `γ`, given that `α` has a discrete topology and `f` is a function from the Cartesian product of `α` and `β` to `γ`, `f` is continuous if and only if, for every element `a` of `α`, the function that maps `y` to `f(a, y)` is continuous. In mathematical terms, this is saying that if a function `f : α × β → γ` is such that the function `y ↦ f(a, y)` is continuous for all `a` in a discrete space `α`, then `f` is continuous, and the converse is also true.
More concisely: A function between two discrete spaces is continuous if and only if the projection functions to each coordinate are continuous.
|
continuous_iff_continuousOn_univ
theorem continuous_iff_continuousOn_univ :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
Continuous f ↔ ContinuousOn f Set.univ
This theorem states that for any two topological spaces α and β and any function `f` from α to β, the function `f` is continuous everywhere if and only if `f` is continuous on the universal set of α. Here, the universal set of α represents the set of all elements of type α. "Continuous" means that the preimage of any open set in β is open in α, and "Continuous on a set" means that the function is continuous at every point within that set.
More concisely: A function from one topological space to another is continuous at all points if and only if it is continuous on the space's universal set.
|
Filter.EventuallyEq.eq_of_nhdsWithin
theorem Filter.EventuallyEq.eq_of_nhdsWithin :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {s : Set α} {f g : α → β} {a : α},
(nhdsWithin a s).EventuallyEq f g → a ∈ s → f a = g a
The theorem `Filter.EventuallyEq.eq_of_nhdsWithin` states that for any two functions `f` and `g` from a type `α` to a type `β`, within a topological space `α`, and a set `s` of type `α`, if `f` is eventually equal to `g` within the neighborhood of a point `a` from the set `s` (`f =ᶠ[nhdsWithin a s] g`), and `a` is an element of the set `s` (`a ∈ s`), then the value of `f` at `a` (`f a`) is equal to the value of `g` at `a` (`g a`).
More concisely: If a point `a` in a set `s` of a topological space and functions `f` and `g` from `α` to `β` satisfy `f =ᶠ[nhdsWithin a s] g`, then `f a = g a`.
|
continuous_if
theorem continuous_if :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {p : α → Prop}
{f g : α → β} [inst_2 : (a : α) → Decidable (p a)],
(∀ a ∈ frontier {x | p x}, f a = g a) →
ContinuousOn f (closure {x | p x}) →
ContinuousOn g (closure {x | ¬p x}) → Continuous fun a => if p a then f a else g a
The theorem `continuous_if` states that for any types `α` and `β` equipped with topological spaces, and any predicate `p : α → Prop`, if we have two functions `f, g : α → β` and each `α` has a decidable predicate `p`, then if `f` and `g` agree on the frontier of the set where `p` holds, and `f` is continuous on the closure of the set where `p` holds while `g` is continuous on the closure of the set where `p` does not hold, then the function which maps each `α` to `f a` if `p a` holds and `g a` otherwise is continuous. In simple terms, it is a theorem about the continuity of a function defined piecewise for two subsets of a topological space.
More concisely: If functions `f` and `g` agree on the boundary and are continuous on the closures of the sets where their respective domain predicates hold, then the piecewise defined function `h : α → β` that maps `f a` to points in `α` where `p(a)` holds and `g a` to points in `α` where `p(a)` does not hold is continuous.
|
ContinuousOn.congr
theorem ContinuousOn.congr :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → β} {s : Set α},
ContinuousOn f s → Set.EqOn g f s → ContinuousOn g s
This theorem states that for any two functions `f` and `g` from a topological space `α` to a topological space `β`, and any set `s` in the space `α`, if the function `f` is continuous on the set `s` and the function `g` is equal to `f` for every point in the set `s`, then the function `g` is also continuous on the set `s`. In mathematical terms, if \(f: \alpha \to \beta\) is continuous on a subset \(S \subset \alpha\) and \(g(x) = f(x)\) for all \(x \in S\), then \(g\) is also continuous on \(S\).
More concisely: If a function `f` is continuous on a subset `S` of a topological space `α` and `g(x) = f(x)` for all `x` in `S`, then `g` is continuous on `S`.
|
Continuous.continuousWithinAt
theorem Continuous.continuousWithinAt :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
{x : α}, Continuous f → ContinuousWithinAt f s x
This theorem states that if a function `f` from a topological space `α` to another topological space `β` is continuous, then it is also continuous at any point `x` within any subset `s` of `α`. Here, continuity at a point within a subset is defined as the property that for any point `x` tending to a limit within the subset `s`, the image of the point under `f`, i.e., `f(x)`, tends towards the limit `f(x)`.
More concisely: If a function `f` is continuous from a topological space `α` to another topological space `β`, then `f` is continuous at any point `x` in `α` with respect to any subset `s` of `α` where `x` has a limit.
|
nhdsWithin_restrict'
theorem nhdsWithin_restrict' :
∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} (s : Set α) {t : Set α},
t ∈ nhds a → nhdsWithin a s = nhdsWithin a (s ∩ t)
This theorem states that for any type `α` equipped with a `TopologicalSpace` structure and any element 'a' of that type, for any two sets `s` and `t` of type `α`, if `t` is a neighborhood of `a`, then the neighborhood within `s` of `a` is equal to the neighborhood within the intersection of `s` and `t` of `a`. In other words, restricting the neighborhood of `a` within set `s` by a set `t` that is itself a neighborhood of `a`, results in the neighborhood within the intersection of `s` and `t` of `a`.
More concisely: For any topological space (α, τ), element a ∈ α, and sets s, t ∈ τ such that t is a neighborhood of a, the neighborhood of a in s is equal to the neighborhood of a in the intersection of s and t.
|
continuousWithinAt_const
theorem continuousWithinAt_const :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {b : β} {s : Set α}
{x : α}, ContinuousWithinAt (fun x => b) s x
This theorem, `continuousWithinAt_const`, states that for any topological spaces `α` and `β`, for any element `b` of `β`, for any subset `s` of `α`, and for any point `x` in `α`, the function that maps every element of `α` to the constant `b` is continuous at the point `x` within the subset `s`. In other words, no matter how `x` changes within the subset `s`, the output of the function remains the same (`b`), thus it is continuous.
More concisely: For any topological spaces α and β, and any constant function f : α → β with image b, the function is continuous at every x in α with respect to the subset s if and only if x ∈ s implies the neighborhoods of x contain only elements mapping to b.
|
nhdsWithin_insert
theorem nhdsWithin_insert :
∀ {α : Type u_1} [inst : TopologicalSpace α] (a : α) (s : Set α),
nhdsWithin a (insert a s) = pure a ⊔ nhdsWithin a s
This theorem, `nhdsWithin_insert`, describes a property of neighborhoods within a given set in a topological space. Specifically, for any type `α`, any instance of a topological space on `α`, any element `a` of type `α`, and any set `s` of type `α`, the neighborhood within the set obtained by inserting `a` into `s` at the point `a` is equal to the join of the singleton set containing just `a` and the neighborhood within `s` at `a`. In other words, adding a point to a set does not change its neighborhood within that set, except at the point that was added.
More concisely: For any topological space and any element, the neighborhood of a point in the set containing that point is equal to the join of the neighborhood of that point in the original set and the singleton set containing that point.
|
ContinuousWithinAt.tendsto_nhdsWithin_image
theorem ContinuousWithinAt.tendsto_nhdsWithin_image :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {x : α}
{s : Set α}, ContinuousWithinAt f s x → Filter.Tendsto f (nhdsWithin x s) (nhdsWithin (f x) (f '' s))
The theorem `ContinuousWithinAt.tendsto_nhdsWithin_image` states that for all types `α` and `β` that are topological spaces, given a function `f` from `α` to `β`, a point `x` in `α`, and a subset `s` of `α`, if `f` is continuous at `x` within `s`, then `f` has the property that for every neighborhood of `f(x)` that intersects with the image of `s` under `f`, the pre-image of this neighborhood under `f` is a neighborhood of `x` within `s`. In other words, as `x` tends to `f(x)` while staying within `s`, `f(x)` tends to `f` of the image of `s`. This is a formalization in Lean 4 of the standard mathematical concept of a function being continuous at a point within a subset.
More concisely: If a function between topological spaces is continuous at a point within a subset, then for every neighborhood of the image of that point intersecting the image of the subset, the pre-image under the function is a neighborhood of the original point within the subset.
|
ContinuousOn.continuousAt
theorem ContinuousOn.continuousAt :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
{x : α}, ContinuousOn f s → s ∈ nhds x → ContinuousAt f x
The theorem `ContinuousOn.continuousAt` states that for all types `α` and `β` equipped with topological structures, for a function `f` from `α` to `β`, a set `s` of `α`, and an element `x` of `α`, if `f` is continuous on `s` and `s` is a neighborhood of `x` (i.e., `s` is in the neighborhood filter of `x`), then `f` is continuous at `x`. In mathematical terms, if a function is continuous on a certain set that contains an open set around a point, then the function is also continuous at that point.
More concisely: If a function is continuous on a neighborhood of a point, then it is continuous at that point.
|
nhdsWithin_eq_map_subtype_coe
theorem nhdsWithin_eq_map_subtype_coe :
∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {a : α} (h : a ∈ s),
nhdsWithin a s = Filter.map Subtype.val (nhds ⟨a, h⟩)
This theorem states that for any topological space `α`, any set `s` in `α`, and any element `a` in `α` such that `a` belongs in `s`, the neighborhood of `a` within `s` is equal to the filter map of the subtype value function on the neighborhood of the subtype of `a` with the property `h` (i.e., `a` belongs in `s`). In other words, it is saying that the concept of neighborhood within a set in topological space corresponds to applying the filter map to the neighborhood of the subtype that consists of elements in the set.
More concisely: For any topological space `α`, set `s ∈ α`, and `a ∈ s`, the neighborhood filter of `a` in `s` is equal to the filter map of the subtype value function on the neighborhood filter of the subtype of `a` in `s`.
|
continuousOn_snd
theorem continuousOn_snd :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set (α × β)},
ContinuousOn Prod.snd s
This theorem states that, for any types `α` and `β` each equipped with a topological space structure, and any set `s` of pairs of elements from `α` and `β`, the second projection function, `Prod.snd`, is continuous on the set `s`. Here, "continuous on a set" means that the function is continuous at each point within that set. In plain terms, this theorem says that picking out the second component of a pair from a set of pairs is a continuous operation.
More concisely: For any topological spaces `α` and `β` and a set `s` of pairs from `α × β`, the second projection function `Prod.snd` is continuous on `s`.
|
continuousOn_iff'
theorem continuousOn_iff' :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α},
ContinuousOn f s ↔ ∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
The theorem `continuousOn_iff'` states that for any types `α` and `β` endowed with a topological structure, a function `f` from `α` to `β`, and a subset `s` of `α`, `f` is continuous on `s` if and only if for every open set `t` in `β`, there exists an open set `u` in `α` such that the preimage of `t` under `f` intersected with `s` is equal to the intersection of `u` and `s`. This can be seen as a way of characterizing continuous functions through the behavior of their preimages on open sets.
More concisely: A function between topological spaces is continuous on a subset if and only if the preimage of every open set under the function intersecting the subset equals the intersection of the subset and some open set in the domain.
|
ContinuousOn.comp
theorem ContinuousOn.comp :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
[inst_2 : TopologicalSpace γ] {g : β → γ} {f : α → β} {s : Set α} {t : Set β},
ContinuousOn g t → ContinuousOn f s → Set.MapsTo f s t → ContinuousOn (g ∘ f) s
This theorem states that for three topological spaces `α`, `β`, and `γ`, if a function `g` from `β` to `γ` is continuous on a set `t`, and another function `f` from `α` to `β` is continuous on a set `s`, and if `f` maps `s` into `t`, then the composition of `g` and `f` (denoted `g ∘ f`) is continuous on the set `s`. This is a composition result regarding the continuity of functions on topological spaces.
More concisely: If functions `f: α → β` and `g: β → γ` are continuous on sets `s subseteq α` and `t subseteq β`, respectively, and `f(s) subseteq t`, then the composition `g ∘ f` is continuous on `s`.
|
ContinuousWithinAt.mono_of_mem
theorem ContinuousWithinAt.mono_of_mem :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s t : Set α}
{x : α}, ContinuousWithinAt f t x → t ∈ nhdsWithin x s → ContinuousWithinAt f s x
The theorem `ContinuousWithinAt.mono_of_mem` states that for any two types `α` and `β` with given topological structures, a function `f` from `α` to `β`, two subsets `s` and `t` of `α`, and a point `x` in `α`, if the function `f` is continuous at the point `x` within the subset `t`, and `t` is in the neighborhood filter of `x` within `s`, then `f` is also continuous at the point `x` within the subset `s`. In other words, if we know that `f` is continuous at `x` when staying within a smaller set `t` and `t` is a part of the local neighborhood of `x` in `s`, we can infer that `f` is continuous at `x` when staying within the larger set `s`.
More concisely: If a function is continuous at a point in a subset and that subset is in the neighborhood filter of that point in a larger subset, then the function is continuous at that point in the larger subset.
|
ContinuousOn.prod
theorem ContinuousOn.prod :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
[inst_2 : TopologicalSpace γ] {f : α → β} {g : α → γ} {s : Set α},
ContinuousOn f s → ContinuousOn g s → ContinuousOn (fun x => (f x, g x)) s
This theorem, `ContinuousOn.prod`, states that for any three types `α`, `β`, and `γ`, each equipped with a topological space structure, and for any two functions `f` from `α` to `β` and `g` from `α` to `γ`, along with a set `s` of type `α`, if `f` and `g` are both continuous on `s`, then the function that maps `x` in `α` to the pair `(f(x), g(x))` in `β x γ` is also continuous on `s`.
In mathematical terms, given two functions `f: α → β` and `g: α → γ` that are continuous on a subset `s` of `α`, the function that maps a point in `s` to a pair consisting of the image of that point under `f` and `g` is also continuous on `s`.
More concisely: Given topological spaces `α`, `β`, and `γ`, and continuous functions `f: α → β` and `g: α → γ` on a subset `s` of `α`, the function `x mapsto (f(x), g(x))` from `s` to `β × γ` is continuous.
|
Inducing.continuousOn_iff
theorem Inducing.continuousOn_iff :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
[inst_2 : TopologicalSpace γ] {f : α → β} {g : β → γ},
Inducing g → ∀ {s : Set α}, ContinuousOn f s ↔ ContinuousOn (g ∘ f) s
This theorem states that for all topological spaces `α`, `β`, and `γ`, and for every function `f` from `α` to `β` and `g` from `β` to `γ`, if `g` induces the topology on `γ` from `β`, then `f` is continuous on a subset `s` of `α` if and only if the composition `g ∘ f` is continuous on the same subset `s`. Here, a function being continuous on a subset means that it is continuous at every point within that subset.
In terms of topology, it implies that the continuity of function compositions is preserved when the second function is inducing.
More concisely: For functions $f: \alpha \to \beta$ and $g: \beta \to \gamma$ with $g$ inducing the topology on $\gamma$ from $\beta$, the subset $s \subseteq \alpha$ is a continuity set for $f$ if and only if $g \circ f$ is a continuity set for $g$ on $s$.
|
Inducing.continuousWithinAt_iff
theorem Inducing.continuousWithinAt_iff :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
[inst_2 : TopologicalSpace γ] {f : α → β} {g : β → γ},
Inducing g → ∀ {s : Set α} {x : α}, ContinuousWithinAt f s x ↔ ContinuousWithinAt (g ∘ f) s x
This theorem states that for any three types `α`, `β`, and `γ` equipped with topological structures (topological spaces), and for any functions `f` from `α` to `β` and `g` from `β` to `γ`, if `g` is an inducing function, then the continuity of `f` within a set `s` at a point `x` is equivalent to the continuity of the composite function `(g ∘ f)` within the same set `s` at the same point `x`. In more mathematical terms, if `g : β → γ` is a function that induces the topology on `β` from `γ`, then a function `f : α → β` is continuous at a point `x` relative to a subset `s` of `α` if and only if the function `g ∘ f : α → γ` is also continuous at `x` relative to `s`.
More concisely: If `g : β → γ` is a topology-inducing function and `s ⊆ α`, then for any `x ∈ s` and continuous functions `f : α → β` and `g ∘ f : α → γ`, the continuity of `f` at `x` if and only if `g ∘ f` is continuous at `x`.
|
ContinuousWithinAt.mono
theorem ContinuousWithinAt.mono :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s t : Set α}
{x : α}, ContinuousWithinAt f t x → s ⊆ t → ContinuousWithinAt f s x
The theorem `ContinuousWithinAt.mono` states that, for any two types `α` and `β` equipped with topological spaces, a function `f` from `α` to `β`, two subsets `s` and `t` of `α`, and a point `x` in `α`, if the function `f` is continuous at the point `x` within the subset `t` and `s` is a subset of `t`, then `f` is also continuous at `x` within the subset `s`. In other words, the continuity of a function at a point within a set is preserved under restriction to a smaller set.
More concisely: If a function is continuous at a point in a subset and the smaller subset is a subcollection of the larger one, then the function is also continuous at that point in the smaller subset.
|
continuousOn_open_iff
theorem continuousOn_open_iff :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α},
IsOpen s → (ContinuousOn f s ↔ ∀ (t : Set β), IsOpen t → IsOpen (s ∩ f ⁻¹' t))
The theorem `continuousOn_open_iff` states that for any two types `α` and `β` that have topological spaces, a function `f` from `α` to `β`, and a set `s` of type `α`, if `s` is an open set, then the function `f` is continuous on `s` if and only if for any open set `t` of type `β`, the preimage of `t` under `f` intersected with `s` is also an open set. In other words, within the context of topology, a function is continuous on an open set if every open set's preimage is also open after intersecting with the original set.
More concisely: A function between topological spaces is continuous on an open set if and only if the preimage of any open set under the function intersecting the original set is also open.
|
Filter.Eventually.self_of_nhdsWithin
theorem Filter.Eventually.self_of_nhdsWithin :
∀ {α : Type u_1} [inst : TopologicalSpace α] {p : α → Prop} {s : Set α} {x : α},
(∀ᶠ (y : α) in nhdsWithin x s, p y) → x ∈ s → p x
This theorem states that for any type `α` with a topological space structure, and for any property `p` on `α`, a set `s` of `α`, and an element `x` of `α`, if it is true that every point `y` in the neighborhood within `s` around `x` eventually satisfies the property `p`, and if `x` is in the set `s`, then `x` itself also satisfies the property `p`. In other words, under these conditions, the property `p` is satisfied not only in the neighborhood of `x` within `s` but also at `x` itself.
More concisely: If `α` is a topological space, `p` is a property on `α`, `s` is a set of `α` containing `x`, and for all `y` in `s` near `x`, `p(y)` holds, then `p(x)` holds.
|
eventually_nhdsWithin_of_eventually_nhds
theorem eventually_nhdsWithin_of_eventually_nhds :
∀ {α : Type u_5} [inst : TopologicalSpace α] {s : Set α} {a : α} {p : α → Prop},
(∀ᶠ (x : α) in nhds a, p x) → ∀ᶠ (x : α) in nhdsWithin a s, p x
The theorem `eventually_nhdsWithin_of_eventually_nhds` states that for any type `α` that has a `TopologicalSpace` structure, any set `s` of this type, any element `a` of this type, and any predicate `p` over elements of this type, if the predicate `p` holds eventually (i.e., outside of a set of measure zero) for elements `x` in the neighborhood of `a`, then `p` also holds eventually for elements `x` in the neighborhood of `a` within the set `s`. In simpler terms, if a property holds true near a point `a`, then it also holds true near `a` when we restrict our attention to a subset `s`.
More concisely: If a property holds eventually in the neighborhood of a point in a topological space and measures zero set excludeds, then it also holds eventually in the neighborhood of that point within any subset of the space.
|
tendsto_nhdsWithin_mono_right
theorem tendsto_nhdsWithin_mono_right :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : β → α} {l : Filter β} {a : α} {s t : Set α},
s ⊆ t → Filter.Tendsto f l (nhdsWithin a s) → Filter.Tendsto f l (nhdsWithin a t)
This theorem, `tendsto_nhdsWithin_mono_right`, states that for any types `α` and `β`, where `α` has a topological space structure, and any function `f` mapping type `β` to `α`, any filter `l` on `β`, any point `a` in `α`, and any sets `s` and `t` of type `α`, if set `s` is a subset of set `t`, then if the function `f` tends to the filter `nhdsWithin a s` (the neighborhood within `s` around `a`) along the filter `l`, it also tends to the filter `nhdsWithin a t` (the neighborhood within `t` around `a`) along the same filter `l`.
In other words, if the function `f` goes to the limit `a` within the smaller set `s` when `l` gets "large", it also goes towards the limit `a` within the larger set `t`.
More concisely: If `f` is a function from `β` to `α` with `α` a topological space, `s ⊆ t` sets in `α`, and `f` tends to `a` in `α` with respect to filter `l` on `β` within `s`, then `f` also tends to `a` within `t` with respect to `l`.
|
IsOpen.nhdsWithin_eq
theorem IsOpen.nhdsWithin_eq :
∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} {s : Set α}, IsOpen s → a ∈ s → nhdsWithin a s = nhds a := by
sorry
The theorem `IsOpen.nhdsWithin_eq` states that for any topological space `α`, a point `a` in `α`, and a set `s` of `α` that is open, if `a` is an element of `s`, then the "neighborhood within" filter of `a` with respect to `s`, denoted by `nhdsWithin a s`, is equal to the neighborhood filter at `a`, denoted by `nhds a`. In other words, if `s` is an open set containing the point `a`, then the neighborhood of `a` within `s` is just the same as the general neighborhood of `a`.
More concisely: For any topological space `α`, point `a` in `α`, and open set `s` in `α`, if `a` belongs to `s`, then `nhdsWithin a s` equals `nhds a`.
|
ContinuousOn.mono_dom
theorem ContinuousOn.mono_dom :
∀ {α : Type u_5} {β : Type u_6} {t₁ t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β},
t₂ ≤ t₁ → ∀ {s : Set α} {f : α → β}, ContinuousOn f s → ContinuousOn f s
This theorem states that if a function is continuous on a certain set given some topologies, then the function remains continuous on that same set with respect to any finer (or stronger) topology on the source space. In other words, if we have a function `f` from a space `α` to a space `β`, with topologies `t₁` and `t₂` on `α` and a topology `t₃` on `β`, and if `f` is continuous on a set `s` under `t₂`, then `f` will also be continuous on `s` under `t₁` if `t₁` is finer than `t₂`. Here, a finer topology on a space means a topology that has more open sets, or equivalently, the continuity of `f` is more strictly determined.
More concisely: If a function is continuous on a set with respect to a weaker topology, then it remains continuous on that set with respect to any finer topology on the domain.
|
ContinuousOn.isOpen_inter_preimage
theorem ContinuousOn.isOpen_inter_preimage :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
{t : Set β}, ContinuousOn f s → IsOpen s → IsOpen t → IsOpen (s ∩ f ⁻¹' t)
This theorem states that for any two types `α` and `β` equipped with topological spaces, given a function `f` from `α` to `β`, a set `s` in `α`, and a set `t` in `β`, if the function `f` is continuous on the set `s`, and both sets `s` and `t` are open, then the intersection of set `s` with the preimage of set `t` under function `f` is also an open set. In mathematical terms, this can be represented as: if we have a continuous function `f: α → β` and two open sets `s ⊆ α` and `t ⊆ β`, then the set `s ∩ f⁻¹(t)` is open in α. Here, `f⁻¹(t)` is the preimage of `t` under `f`, meaning the set of all elements in `α` that `f` maps into `t`.
More concisely: If `f: α → β` is a continuous function between topological spaces `α` and `β`, and `s ⊆ α` and `t ⊆ β` are open sets, then the intersection of `s` with the preimage of `t` under `f` is an open set in `α`.
|
nhdsWithin_basis_open
theorem nhdsWithin_basis_open :
∀ {α : Type u_1} [inst : TopologicalSpace α] (a : α) (t : Set α),
(nhdsWithin a t).HasBasis (fun u => a ∈ u ∧ IsOpen u) fun u => u ∩ t
This theorem, `nhdsWithin_basis_open`, states that for any type `α` that has a topological space structure, any element `a` of type `α`, and any set `t` of type `α`, the "neighborhood within" filter (`nhdsWithin`) has a basis. This basis is characterized by the sets `u` that contain the point `a` and are open in the topological space. The elements of this basis are the intersections of `u` and `t`. In mathematical terms, this theorem is saying that for any point in a topological space and any subset of that space, we can find a fundamental system of neighborhoods (basis of the filter) for the point, consisting of open sets containing the point, whose intersections with the given subset form the neighborhoods within the subset.
More concisely: For any point `a` in a topological space `α` and any subset `t` of `α`, the filter of neighborhoods of `a` within `t` has a basis consisting of open sets containing `a` whose intersections with `t` are the neighborhoods within `t`.
|
pure_le_nhdsWithin
theorem pure_le_nhdsWithin :
∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} {s : Set α}, a ∈ s → pure a ≤ nhdsWithin a s
This theorem states that for any type `α` that has a topological space structure (indicated by `[TopologicalSpace α]`), for any element `a` of `α` and any set `s` of `α`, if `a` is an element of `s` (expressed as `a ∈ s`), then the pure filter of `a` is less than or equal to the "neighborhood within" filter of `a` within `s` (expressed as `pure a ≤ nhdsWithin a s`). Here, the "neighborhood within" filter of `a` within `s` refers to the intersection of `s` and a neighborhood of `a`.
More concisely: For any topological space `α` and element `a` in `α`, if `a` belongs to a set `s`, then the pure filter of `a` is contained in the neighborhood filter of `a` within `s`.
|
ContinuousOn.restrict_mapsTo
theorem ContinuousOn.restrict_mapsTo :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
{t : Set β}, ContinuousOn f s → ∀ (ht : Set.MapsTo f s t), Continuous (Set.MapsTo.restrict f s t ht)
The theorem `ContinuousOn.restrict_mapsTo` states that for any types `α` and `β`, both endowed with a topological structure, a function `f` from `α` to `β`, and sets `s` of `α` and `t` of `β`, if `f` is continuous on `s` and the image of `s` under `f` is contained in `t` (expressed as `Set.MapsTo f s t`), then the function `f` restricted to `s` and `t` is continuous. In other words, the continuity of `f` on `s` and the mapping condition between `s` and `t` ensure the continuity of the restricted function.
More concisely: If a function between topological spaces is continuous on a set and maps that set to another set, then the restriction of the function to that set is continuous.
|
tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
theorem tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {a : α} {l : Filter β} {s : Set α} (f : β → α),
Filter.Tendsto f l (nhds a) → (∀ᶠ (x : β) in l, f x ∈ s) → Filter.Tendsto f l (nhdsWithin a s)
This theorem, `tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within`, states that for all types `α` and `β` with `α` being a type equipped with a topological space structure, given an element `a` of type `α`, a filter `l` on type `β`, a set `s` of elements of type `α`, and a function `f` mapping elements from `β` to `α`, if the function `f` tends to `nhds a` under the filter `l` (i.e., the limit of `f` as elements approach `a` exists and is defined by the neighbourhood filter at `a`) and all elements from `l` eventually fall into the set `s` (i.e., for all large enough elements), then `f` also tends to the neighbourhood within `s` of `a` under the filter `l`. In other words, the limit of `f` as elements approach `a` within the set `s` also exists and is defined by the intersection of `s` and a neighbourhood of `a`.
More concisely: If a function `f` tends to the neighborhood filter of `a` in a topological space `α` under a filter `l`, and all elements in `l` eventually belong to a set `s`, then `f` tends to the neighborhood filter of `a` within `s` under `l`.
|
nhdsWithin_le_nhds
theorem nhdsWithin_le_nhds :
∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} {s : Set α}, nhdsWithin a s ≤ nhds a
This theorem states that for any type `α` which has a topological space structure, for any element `a` of type `α`, and for any set `s` of elements of `α`, the neighborhood within `s` at `a`, denoted `nhdsWithin a s`, is contained within or equal to the neighborhood at `a`, denoted `nhds a`. In other words, all sets that contain the intersection of `s` and a neighborhood of `a` are also neighborhoods of `a`.
More concisely: For any topological space `(α, τ)` and any `a ∈ α`, the neighborhood filter of `a`, `nhds a`, contains the neighborhood filter within `a` of any set `s ⊆ α`, `nhdsWithin a s`.
|
ContinuousWithinAt.preimage_mem_nhdsWithin''
theorem ContinuousWithinAt.preimage_mem_nhdsWithin'' :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {x : α}
{y : β} {s t : Set β},
ContinuousWithinAt f (f ⁻¹' s) x → t ∈ nhdsWithin y s → y = f x → f ⁻¹' t ∈ nhdsWithin x (f ⁻¹' s)
This theorem states that for any types `α` and `β` that have topological space structures, any function `f` from `α` to `β`, any points `x` in `α` and `y` in `β`, and any sets `s` and `t` of `β`, if `f` is continuous at `x` within the preimage of `s` under `f`, and if `t` is in the neighborhood within `s` of `y`, and if `y` is the image of `x` under `f`, then the preimage of `t` under `f` is in the neighborhood within the preimage of `s` under `f` of `x`. In simpler terms, if a function is continuous at a point and a certain set is nearby, then the preimage of that set is also nearby.
More concisely: If a continuous function maps a point to a neighboring image point in a topological space, then the preimage of a neighborhood of that image point is a neighborhood of the original point.
|
ContinuousOn.if'
theorem ContinuousOn.if' :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set α} {p : α → Prop}
{f g : α → β} [inst_2 : (a : α) → Decidable (p a)],
(∀ a ∈ s ∩ frontier {a | p a},
Filter.Tendsto f (nhdsWithin a (s ∩ {a | p a})) (nhds (if p a then f a else g a))) →
(∀ a ∈ s ∩ frontier {a | p a},
Filter.Tendsto g (nhdsWithin a (s ∩ {a | ¬p a})) (nhds (if p a then f a else g a))) →
ContinuousOn f (s ∩ {a | p a}) →
ContinuousOn g (s ∩ {a | ¬p a}) → ContinuousOn (fun a => if p a then f a else g a) s
This theorem states that given two types `α` and `β` with respective topological spaces, a set `s` of type `α`, a predicate `p : α → Prop`, and two functions `f, g : α → β`, if it is decidable for each element `a` of type `α` whether it satisfies the predicate `p a`, then the following conditions hold:
1. For every `a` in the intersection of `s` and the frontier of the set where `p a` holds, the function `f` tends to the neighborhood of `(if p a then f a else g a)` within the intersection of `s` and the set where `p a` holds.
2. For every `a` in the intersection of `s` and the frontier of the set where `p a` holds, the function `g` tends to the neighborhood of `(if p a then f a else g a)` within the intersection of `s` and the set where `p a` does not hold.
3. The function `f` is continuous on the intersection of `s` and the set where `p a` holds.
4. The function `g` is continuous on the intersection of `s` and the set where `p a` does not hold.
If all these conditions are met, then the piecewise function defined as `(fun a => if p a then f a else g a)` is continuous on the set `s`. In plain language, if `f` and `g` behave well at the boundary between where `p a` is true and false, and are continuous where they are respectively true and false, then the function that is `f` where `p a` is true and `g` where `p a` is false is continuous.
More concisely: Given types `α`, `β`, a set `s` of type `α`, a decidable predicate `p : α → Prop`, and continuous functions `f, g : α → β`, if `f` and `g` tend to the same limit on the frontier of `s` where `p` is undefined and are continuous on `s` where `p` holds respectively, then the piecewise function `(fun a => if p a then f a else g a)` is continuous on `s`.
|
eventually_nhds_nhdsWithin
theorem eventually_nhds_nhdsWithin :
∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} {s : Set α} {p : α → Prop},
(∀ᶠ (y : α) in nhds a, ∀ᶠ (x : α) in nhdsWithin y s, p x) ↔ ∀ᶠ (x : α) in nhdsWithin a s, p x
This theorem, `eventually_nhds_nhdsWithin`, states that for any topological space `α`, a point `a` in that space, a set `s` of `α`, and a property `p` that elements of `α` might satisfy, the following two conditions are equivalent:
1. For any point `y` in the neighborhood of `a`, eventually for every point `x` in the intersection of `s` and the neighborhood of `y`, `p` holds for `x`.
2. Eventually for every point `x` in the intersection of `s` and the neighborhood of `a`, `p` holds for `x`.
Here, "eventually" is used in the sense of filter theory: a property holds eventually in a filter if the property is true within some element of the filter, and a neighborhood of a point is an open set containing that point.
More concisely: For any topological space, point, set, and property, the two conditions are equivalent: the property holds eventually for all points in the intersection of the set and the neighborhood of any point in the neighborhood of the given point, if and only if the property holds eventually for all points in the intersection of the set and the neighborhood of the given point.
|
tendsto_nhdsWithin_of_tendsto_nhds
theorem tendsto_nhdsWithin_of_tendsto_nhds :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → β} {a : α} {s : Set α} {l : Filter β},
Filter.Tendsto f (nhds a) l → Filter.Tendsto f (nhdsWithin a s) l
The theorem `tendsto_nhdsWithin_of_tendsto_nhds` states that for any types `α` and `β` with `α` being a topological space, any function `f` from `α` to `β`, any point `a` in `α`, any set `s` of `α`, and any filter `l` on `β`, if the function `f` tends to the filter `l` at the neighborhood of `a` (`nhds a`), then it also tends to `l` at the intersection of `s` and a neighborhood of `a` (`nhdsWithin a s`). In other words, if `f` converges to `l` as we approach `a`, it still converges to `l` even if we only approach `a` within the subset `s` of `α`.
More concisely: If a function from a topological space to another tends to a filter at a point's neighborhood, then it also tends to that filter at the intersection of any subset and a neighborhood of the point.
|
ContinuousWithinAt.continuousAt
theorem ContinuousWithinAt.continuousAt :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
{x : α}, ContinuousWithinAt f s x → s ∈ nhds x → ContinuousAt f x
This theorem states that for any given types `α` and `β` that have topological space structures, if a function `f` from `α` to `β` is continuous at a point `x` within a subset `s` of `α` (i.e., the value of `f` at `x` approaches the value of `f` at `x₀` as `x` tends to `x₀` within `s`), and if `s` is a neighborhood of `x` (i.e., `s` contains an open set around `x`), then `f` is continuous at `x` (i.e., the value of `f` at `x` approaches the value of `f` at `x₀` as `x` tends to `x₀` without restriction).
More concisely: If a continuous function between topological spaces `f : α → β` is continuous at a point `x` in a neighborhood `s ⊆ α` of `x`, then `f` is continuous at `x`.
|
nhdsWithin_mono
theorem nhdsWithin_mono :
∀ {α : Type u_1} [inst : TopologicalSpace α] (a : α) {s t : Set α}, s ⊆ t → nhdsWithin a s ≤ nhdsWithin a t := by
sorry
This theorem states that for any type `α` equipped with a topology and any element `a` of this type, if we have two sets `s` and `t` of `α` such that `s` is a subset of `t`, then the neighborhood within `s` of `a` is a subset of the neighborhood within `t` of `a`. In other words, it says that restricting the neighborhood of `a` to a smaller set corresponds to a smaller "neighborhood within". This theorem is a statement about the interaction between subsets and the "neighborhood within" filter in a topological space.
More concisely: For any topological space (α,τ), and elements s ⊆ t and a ∈ α, the neighborhood filter Nbhd(a)|s of a in s is contained in the neighborhood filter Nbhd(a)|t of a in t.
|
ContinuousAt.comp_continuousWithinAt
theorem ContinuousAt.comp_continuousWithinAt :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
[inst_2 : TopologicalSpace γ] {g : β → γ} {f : α → β} {s : Set α} {x : α},
ContinuousAt g (f x) → ContinuousWithinAt f s x → ContinuousWithinAt (g ∘ f) s x
The theorem `ContinuousAt.comp_continuousWithinAt` states that for any three topological spaces `α`, `β`, and `γ`, and any two functions `g: β → γ` and `f: α → β`, as well as a set `s` of the type `α` and an element `x` of type `α`, if the function `g` is continuous at the point `(f x)` and the function `f` is continuous within the set `s` at the point `x`, then the composition of `g` and `f`, denoted by `(g ∘ f)`, is also continuous within the set `s` at the point `x`. In other words, the continuity of `g` at `(f x)` and the continuity of `f` at `x` within `s` implies the continuity of the composition `(g ∘ f)` at `x` within `s`.
More concisely: If functions `f: α → β` is continuous at `x ∈ α` within a set `s ⊆ α` and `g: β → γ` is continuous at `f x ∈ β`, then their composition `g ∘ f` is continuous at `x` within `s`.
|
nhdsWithin_inter_of_mem
theorem nhdsWithin_inter_of_mem :
∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} {s t : Set α},
s ∈ nhdsWithin a t → nhdsWithin a (s ∩ t) = nhdsWithin a t
This theorem states that for any type 'α' equipped with a topology, and any element 'a' of this type, along with two sets 's' and 't' of this type, if 's' is in the neighborhood within 't' of 'a', then the neighborhood within the intersection of 's' and 't' of 'a' is equal to the neighborhood within 't' of 'a'. In other words, within a topological space, if a set 's' is found within a certain neighborhood of 'a' confined to another set 't', then the neighborhood of 'a' within the intersection of 's' and 't' doesn't change the original neighborhood within 't' of 'a'.
More concisely: Given a topological space 'α' and an element 'a' in it, if 's' is a neighborhood of 'a' contained in 't', then the neighborhood of 'a' in the intersection of 's' and 't' equals the neighborhood of 'a' in 't'.
|
continuousWithinAt_iff_continuousAt_restrict
theorem continuousWithinAt_iff_continuousAt_restrict :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {x : α}
{s : Set α} (h : x ∈ s), ContinuousWithinAt f s x ↔ ContinuousAt (s.restrict f) ⟨x, h⟩
The theorem `continuousWithinAt_iff_continuousAt_restrict` states that for all types `α` and `β`, topological spaces `inst` and `inst_1` defined on these types, a function `f` from `α` to `β`, a point `x` of type `α`, and a set `s` of type `α`, if `x` is an element of `s`, then the function `f` is continuous at the point `x` within the set `s` if and only if when the domain of the function `f` is restricted to the set `s`, the function is continuous at the point `x`. In other words, restricting the domain of a function to a subset does not affect the continuity of the function at a point within that subset.
More concisely: For all types `α` and `β`, topological spaces `inst` and `inst_1` on `α`, function `f : α → β`, point `x : α`, and set `s ⊆ α` containing `x`, the function `f` is continuous at `x` within `s` if and only if the restriction of `f` to `s` is continuous at `x`.
|
nhdsWithin_inter
theorem nhdsWithin_inter :
∀ {α : Type u_1} [inst : TopologicalSpace α] (a : α) (s t : Set α),
nhdsWithin a (s ∩ t) = nhdsWithin a s ⊓ nhdsWithin a t
The theorem `nhdsWithin_inter` states that for any type `α` that is a topological space and for any element `a` of that type, as well as for any two sets `s` and `t` of that type, the neighborhood within the intersection of `s` and `t` at `a` is equal to the intersection of the neighborhoods within `s` and `t` at `a`. In other words, it establishes the equality between the topological neighborhood within the intersection of two sets and the intersection of the topological neighborhoods within each set, for a given point. This is akin to the distributive property in algebra.
More concisely: For any topological space `α` and elements `a` in `α`, the neighborhood filter of `a` in the intersection of sets `s` and `t` equals the intersection of the neighborhood filters of `a` in `s` and `t`.
|
IsOpen.ite
theorem IsOpen.ite :
∀ {α : Type u_1} [inst : TopologicalSpace α] {s s' t : Set α},
IsOpen s → IsOpen s' → s ∩ frontier t = s' ∩ frontier t → IsOpen (t.ite s s')
The theorem `IsOpen.ite` states that for any type `α` equipped with a topology, and for any sets `s`, `s'`, and `t` of type `α`, if `s` and `s'` are open sets and the intersection of `s` with the frontier of `t` is equal to the intersection of `s'` with the frontier of `t`, then the set resulting from the `Set.ite` function applied to `t`, `s`, and `s'` is an open set. In other words, it states the openness of the set formed by taking the elements of `s` that are in `t` and the elements of `s'` that are not in `t`, given certain conditions on `s`, `s'`, and `t`.
More concisely: If sets `s`, `s'`, and `t` in a topological space are open and their frontier intersections with `t` are equal, then the set obtained by applying `Set.ite` function to `t`, `s`, and `s'` is open.
|
tendsto_nhds_of_tendsto_nhdsWithin
theorem tendsto_nhds_of_tendsto_nhdsWithin :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : β → α} {a : α} {s : Set α} {l : Filter β},
Filter.Tendsto f l (nhdsWithin a s) → Filter.Tendsto f l (nhds a)
This theorem, `tendsto_nhds_of_tendsto_nhdsWithin`, states that for any types `α` and `β`, where `α` is equipped with a topological space structure, and any function `f` from `β` to `α`, any point `a` in `α`, any set `s` in `α`, and any filter `l` on `β`, if `f` tends towards the neighborhood filter of `a` within the set `s` under the filter `l`, then `f` also tends towards the neighborhood filter of `a` under the filter `l`. In other words, if the values of `f` get arbitrarily close to `a` when the input values (from `β`) are taken from `l` and the outputs are within `s`, then `f` will get arbitrarily close to `a` when the input values are just taken from `l`, regardless of whether the outputs are within `s`.
More concisely: If a function `f` from `β` to `α` (where `α` is a topological space) tends towards the neighborhood filter of `a` in `α` within the set `s` under filter `l` on `β`, then `f` tends towards the neighborhood filter of `a` under filter `l`.
|
ContinuousWithinAt.tendsto_nhdsWithin
theorem ContinuousWithinAt.tendsto_nhdsWithin :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {x : α}
{s : Set α} {t : Set β},
ContinuousWithinAt f s x → Set.MapsTo f s t → Filter.Tendsto f (nhdsWithin x s) (nhdsWithin (f x) t)
The theorem `ContinuousWithinAt.tendsto_nhdsWithin` states that for every topological spaces `α` and `β`, function `f : α → β`, point `x : α`, and sets `s : Set α` and `t : Set β`, if the function `f` is continuous at point `x` within the set `s` and the image of `s` under `f` is contained in `t`, then the limit of function `f` as `x` approaches within `s` equals the limit of `f(x)` as it approaches within `t`. In other words, it asserts the image of a neighborhood within a set under a continuous function is itself a neighborhood within the image of the set.
More concisely: If a continuous function restricted to a set maps that set's neighborhoods to neighborhoods in the image set, then the limit of the function as the input approaches within the set equals the limit of the function's image as the image approaches within the image set.
|
ContinuousOn.continuousWithinAt
theorem ContinuousOn.continuousWithinAt :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
{x : α}, ContinuousOn f s → x ∈ s → ContinuousWithinAt f s x
This theorem states that for any given types `α` and `β` with topological structures, a function `f` from `α` to `β`, a set `s` of `α`, and an element `x` of `α`, if the function `f` is continuous on the set `s`, and the element `x` is a member of the set `s`, then the function `f` is continuous at the point `x` within the set `s`. In mathematical terms, this means that the function `f` tends to the limit `f(x)` as `x` approaches `x₀` within the set `s`.
More concisely: If `f` is a continuous function from topological spaces `α` to `β`, `x` is an element of the domain `α`, and `s` is a subset of `α` where `f` is continuous at `x`, then `f` is continuous at `x` with respect to the subspace topology of `s`.
|
mem_of_mem_nhdsWithin
theorem mem_of_mem_nhdsWithin :
∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} {s t : Set α}, a ∈ s → t ∈ nhdsWithin a s → a ∈ t
This theorem asserts that for any type `α` that has a topological space structure, and any elements `a` of type `α` and sets `s` and `t` of type `Set α`, if `a` is an element of `s` and `t` is in the filter of neighborhood within `s` of `a` (denoted by `nhdsWithin a s`), then `a` is also an element of `t`. In other words, if `a` is in some set `s` and `t` is within the neighborhood of `a` restricted to `s`, then `a` is also in `t`. This theorem is part of the foundation for the understanding of neighborhood filters in a topological space.
More concisely: For any topological space `α` and elements `a ∈ α`, `s ∈ Set α`, and `t ∈ nhdsWithin a s`, we have `a ∈ t`.
|
ContinuousWithinAt.prod
theorem ContinuousWithinAt.prod :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
[inst_2 : TopologicalSpace γ] {f : α → β} {g : α → γ} {s : Set α} {x : α},
ContinuousWithinAt f s x → ContinuousWithinAt g s x → ContinuousWithinAt (fun x => (f x, g x)) s x
The theorem `ContinuousWithinAt.prod` states that for any types `α`, `β`, and `γ` equipped with topological space structures, given two functions `f: α → β` and `g: α → γ`, and a set `s` of type `α` with a particular element `x` in `α`; if the function `f` is continuous within the set `s` at the point `x` and similarly the function `g` is also continuous within `s` at `x`, then the function that maps `x` to the ordered pair `(f x, g x)` is also continuous within `s` at the point `x`. In other words, the product of two continuous functions remains continuous within the same subset.
More concisely: If functions `f: α → β` and `g: α → γ` are continuous at a point `x` in `α` within a set `s` subsets of `α`, then the function `(f, g): α → β × γ` mapping `x` to `(f x, g x)` is continuous at `x`.
|
ContinuousOn.mono
theorem ContinuousOn.mono :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s t : Set α},
ContinuousOn f s → t ⊆ s → ContinuousOn f t
This theorem states that for any two types `α` and `β` with topological space structures, and a function `f` from `α` to `β`, if `f` is continuous on a set `s` of `α`, and `t` is a subset of `s`, then `f` is also continuous on `t`. In mathematical terms, this expresses the idea that the continuity of a function on a set implies its continuity on all subsets of that set.
More concisely: If `f` is a continuous function from topological space `α` to topological space `β`, and `s` is a subset of `α`, then `f` restricted to `s` is continuous.
|
ContinuousOn.preimage_isClosed_of_isClosed
theorem ContinuousOn.preimage_isClosed_of_isClosed :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
{t : Set β}, ContinuousOn f s → IsClosed s → IsClosed t → IsClosed (s ∩ f ⁻¹' t)
This theorem states that for any two types `α` and `β` equipped with topological structures, a function `f` from `α` to `β`, and sets `s` of type `α` and `t` of type `β`, if the function `f` is continuous on the set `s`, and both sets `s` and `t` are closed, then the intersection of set `s` and the preimage of set `t` under the function `f` is also closed. Here, the preimage of set `t` under function `f` consists of all the elements in `α` that get mapped to elements in `t` by `f`.
More concisely: If `f` is a continuous function between topological spaces `(α, τα)` and `(β, τβ)`, `s ⊆ α` and `t ⊆ β` are closed sets, then the preimage `f⁻¹(t)` of `t` under `f` and `s` have a closed intersection.
|
eventually_mem_nhdsWithin
theorem eventually_mem_nhdsWithin :
∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} {s : Set α}, ∀ᶠ (x : α) in nhdsWithin a s, x ∈ s
This theorem, `eventually_mem_nhdsWithin`, states that for any type `α` that has a topological space structure, any point `a` of type `α`, and any set `s` of type `α`, eventually, for all points `x` in the neighborhood within `s` of `a` (represented as `nhdsWithin a s`), `x` belongs to set `s`. In other words, it guarantees that in the vicinity of any point `a` within a set `s` in a topological space, all the points are eventually elements of `s`.
More concisely: For any topological space `(α, τ)` and point `a` in `α` with `s ∈ τ`, eventually all points in the neighborhood `nhdsWithin a s` belong to `s`.
|
ContinuousOn.comp_continuous
theorem ContinuousOn.comp_continuous :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
[inst_2 : TopologicalSpace γ] {g : β → γ} {f : α → β} {s : Set β},
ContinuousOn g s → Continuous f → (∀ (x : α), f x ∈ s) → Continuous (g ∘ f)
This theorem states that given three topological spaces `α`, `β`, and `γ`, along with two functions `f : α → β` and `g : β → γ`, and a set `s` in `β`, if the function `g` is continuous on the set `s`, and the function `f` is continuous everywhere and maps every element of `α` into the set `s`, then the composition function `g ∘ f` (which maps `α` to `γ` through `β`) is also continuous everywhere. In other words, the continuity of a composite function is preserved when the component functions are continuous, with the first function mapping into a set where the second function is continuous.
More concisely: If functions `f : α → β`, `g : β → γ` are continuous, `s ⊆ β`, and `f` maps every `x ∈ α` into `s` and `g` is continuous on `s`, then `g ∘ f` is continuous.
|
nhdsWithin_le_of_mem
theorem nhdsWithin_le_of_mem :
∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} {s t : Set α},
s ∈ nhdsWithin a t → nhdsWithin a t ≤ nhdsWithin a s
This theorem states that for any type `α` that has a topological space structure, and any elements `a` of type `α`, and for any sets `s` and `t` of type `α`; if `s` is a member of the "neighborhood within" filter of `a` and `t`, then the "neighborhood within" filter of `a` and `t` is less than or equal to the "neighborhood within" filter of `a` and `s`. In mathematical terms, if `s` is in the intersection of `t` and a neighborhood of `a`, then every set that is in the intersection of `t` and a neighborhood of `a` is also in the intersection of `s` and a neighborhood of `a`.
More concisely: If `a` is an element of a topological space `α`, `s` and `t` are subsets of `α` such that `s` is a neighborhood of `a` containing `t`, then for any neighborhood `U` of `a`, `s ∩ U` is a subset of `t ∩ U`.
|
Mathlib.Topology.ContinuousOn._auxLemma.32
theorem Mathlib.Topology.ContinuousOn._auxLemma.32 :
∀ {α : Type u_1} {β : Type u_2} {p : α × β → Prop}, (∀ (x : α × β), p x) = ∀ (a : α) (b : β), p (a, b)
This theorem, `Mathlib.Topology.ContinuousOn._auxLemma.32`, declares that for any types `α` and `β` and any proposition `p` about a pair of elements from `α` and `β`, stating that the proposition `p` holds for all pairs `(x : α × β)` is equivalent to stating that for every individual element `a` from `α` and `b` from `β`, the proposition `p` holds for the pair `(a, b)`. In other words, we can check a property for all pairs either pair by pair or element by element.
More concisely: The theorem asserts that for a proposition `p` about pairs of elements from types `α` and `β`, it holds if and only if it holds for every pair `(a, b)` where `a` is from `α` and `b` is from `β`.
|
ContinuousOn.restrict
theorem ContinuousOn.restrict :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α},
ContinuousOn f s → Continuous (s.restrict f)
This theorem states that for any two types `α` and `β`, given that `α` and `β` are both topological spaces, if a function `f : α → β` is continuous on a subset `s` of `α` (i.e., it is continuous at every point in `s`), then the function `f` remains continuous when its domain is restricted to the set `s`. In other words, if a function is continuous over a specific set in its domain, then the restriction of that function to that set is also continuous.
More concisely: If a function between topological spaces is continuous on a subset, then its restriction to that subset is also continuous.
|
nhdsWithin_hasBasis
theorem nhdsWithin_hasBasis :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {p : β → Prop} {s : β → Set α} {a : α},
(nhds a).HasBasis p s → ∀ (t : Set α), (nhdsWithin a t).HasBasis p fun i => s i ∩ t
The theorem `nhdsWithin_hasBasis` states that for any types `α` and `β` and any topological space on `α`, given a predicate `p` on `β`, a function `s` from `β` to sets of `α`, and a point `a` in `α`, if the neighborhood filter (`nhds a`) has a basis defined by `p` and `s`, then for any set `t` of `α`, the "neighborhood within" filter (`nhdsWithin a t`) also has a basis defined by `p` and the intersection between `s i` and `t` for every `i` in `β` fulfilling the predicate `p`. In simple terms, this theorem says that if a neighborhood filter of a point has a certain basis, then the basis for the filter of the neighborhood within a particular set is composed by the intersection of this set with the sets of the original basis.
More concisely: If a neighborhood filter at a point in a topological space has a basis given by a predicate and a function, then the neighborhood filter within a set has a basis given by the intersection of the set with the basis elements fulfilling the predicate.
|
mem_nhdsWithin_iff_exists_mem_nhds_inter
theorem mem_nhdsWithin_iff_exists_mem_nhds_inter :
∀ {α : Type u_1} [inst : TopologicalSpace α] {t : Set α} {a : α} {s : Set α},
t ∈ nhdsWithin a s ↔ ∃ u ∈ nhds a, u ∩ s ⊆ t
This theorem states that for any topological space `α`, given a set `s` in `α` and an element `a` in `α`, a set `t` is in the filter of neighborhoods within `s` of `a` (i.e., `t` is a neighborhood of `a` within `s`) if and only if there exists a set `u` which is a neighborhood of `a` (i.e., `u` is in the filter of all neighborhoods of `a`) such that the intersection of `u` and `s` is contained within `t`. In other words, `t` is a "local" neighborhood of `a` within `s` precisely when `t` contains the intersection of `s` and some "global" neighborhood of `a`.
More concisely: For any topological space `α`, a set `t` is a neighborhood of `a` in `s` (i.e., in the filter of neighborhoods of `a` within `s`) if and only if there exists a neighborhood `u` of `a` such that `u ∩ s` is contained in `t`.
|
mem_nhdsWithin
theorem mem_nhdsWithin :
∀ {α : Type u_1} [inst : TopologicalSpace α] {t : Set α} {a : α} {s : Set α},
t ∈ nhdsWithin a s ↔ ∃ u, IsOpen u ∧ a ∈ u ∧ u ∩ s ⊆ t
This theorem states that for any type `α`, with a given topological structure, and any sets `t` and `s` from `α` and an element `a` from `α`, `t` is in the neighborhood within `s` of `a` if and only if there exists a set `u` such that `u` is open, `a` is in `u`, and the intersection of `u` and `s` is a subset of `t`. In other words, a set is in the neighborhood within another set of a certain point if and only if it contains the intersection of that other set with some open set containing the point.
More concisely: For any topological space `(α, τ)`, point `a` in `α`, and sets `t, s` in `α`, `t` is a neighborhood of `a` within `s` if and only if there exists an open set `u` containing `a` such that `t` is a subset of `u ∩ s`.
|
Continuous.continuousOn
theorem Continuous.continuousOn :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α},
Continuous f → ContinuousOn f s
The theorem `Continuous.continuousOn` asserts that for any two topological spaces `α` and `β`, and a function `f` from `α` to `β`, if `f` is continuous over the entire domain `α`, then `f` is also continuous on any subset `s` of its domain. In mathematical terms, if a function is continuous in a topological sense, then it remains continuous when restricted to any subset of its original domain.
More concisely: If a function is continuous on its entire domain, then it is continuous on any of its subsets.
|
nhdsWithin_univ
theorem nhdsWithin_univ : ∀ {α : Type u_1} [inst : TopologicalSpace α] (a : α), nhdsWithin a Set.univ = nhds a := by
sorry
This theorem states that for any type `α` which has a topological space structure and for any element `a` of type `α`, the neighborhood within the universal set `Set.univ` at the point `a` is equivalent to the neighborhood of `a`. In mathematical terms, if we take the intersection of the universal set and a neighborhood of `a`, it is just the neighborhood of `a` itself. This is because the universal set contains all elements of `α`, including all points in any neighborhood of `a`.
More concisely: For any topological space `(α, τ)` and point `a ∈ α`, the neighborhood filter of `a` is equal to the subset filter of `Set.univ` restricted to the neighborhoods of `a`.
|
nhdsWithin_union
theorem nhdsWithin_union :
∀ {α : Type u_1} [inst : TopologicalSpace α] (a : α) (s t : Set α),
nhdsWithin a (s ∪ t) = nhdsWithin a s ⊔ nhdsWithin a t
This theorem states that for any given topological space `α`, any point `a` in that space, and any two sets `s` and `t` in that space, the neighborhood within the union of `s` and `t` at the point `a` is equal to the supremum (join) of the neighborhood within `s` at `a` and the neighborhood within `t` at `a`. In other words, it's describing how the "nearness" to a point in a union of two sets can be described in terms of the "nearness" to that point in each of the individual sets. This is a property of neighborhoods in a topological space.
More concisely: For any topological space `α`, point `a` in `α`, and sets `s` and `t` in `α`, the neighborhood of `a` in `s ∪ t` is equal to the join (supremum) of the neighborhood of `a` in `s` and the neighborhood of `a` in `t`.
|
tendsto_nhdsWithin_iff
theorem tendsto_nhdsWithin_iff :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {a : α} {l : Filter β} {s : Set α} {f : β → α},
Filter.Tendsto f l (nhdsWithin a s) ↔ Filter.Tendsto f l (nhds a) ∧ ∀ᶠ (n : β) in l, f n ∈ s
The theorem `tendsto_nhdsWithin_iff` states that for any topological space `α`, filter `l` on a type `β`, a set `s` of `α`, and a function `f` from `β` to `α` mapping elements of the filter to the topological space, the function `f` tends to the neighborhood within `s` of a point `a` in `α` under the filter `l` if and only if `f` tends to the neighborhood of `a` under `l` and, eventually, for all elements `n` in `l`, `f n` belongs to `s`. In mathematical notation, this could be written as $\lim_{n \to l} f(n) \in \mathcal{N}_s(a) \iff \left(\lim_{n \to l} f(n) \in \mathcal{N}(a) \land \forall n \in l, f(n) \in s \right)$, where $\mathcal{N}_s(a)$ and $\mathcal{N}(a)$ denote the neighborhood within `s` of `a` and the neighborhood of `a`, respectively.
More concisely: A function from a filter to a topological space tends to the neighborhood within a set of the space of a point if and only if it tends to the neighborhood of the point and all elements of the filter belong to the set.
|
nhdsWithin_eq_nhds
theorem nhdsWithin_eq_nhds :
∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} {s : Set α}, nhdsWithin a s = nhds a ↔ s ∈ nhds a
This theorem states that for any type `α` with a topological space structure, any element `a` of `α`, and any set `s` of `α`, the neighborhood within `s` of `a` is equal to the neighborhood of `a` if and only if `s` is a neighborhood of `a`. In other words, it describes a condition under which a "restricted" neighborhood (one confined to a certain set) is equivalent to a general neighborhood in a topological space.
More concisely: For any topological space `(α, τ)` and element `a` in `α`, a set `s` is a neighborhood of `a` if and only if the neighborhood of `a` within `s` is equal to `s`.
|
nhdsWithin_empty
theorem nhdsWithin_empty : ∀ {α : Type u_1} [inst : TopologicalSpace α] (a : α), nhdsWithin a ∅ = ⊥
This theorem states that for any type `α` that has a `TopologicalSpace` instance and for any element `a` of this type, the "neighborhood within" of `a` with respect to the empty set is the bottom filter. In other words, in a topological space, the intersection of an empty set with a neighborhood of any point is considered to be the most trivial filter, represented as `⊥`, which basically means it contains no open sets.
More concisely: In a topological space, the intersection of the empty set with any neighborhood of a point is the bottom filter.
|
nhdsWithin_inter_of_mem'
theorem nhdsWithin_inter_of_mem' :
∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} {s t : Set α},
t ∈ nhdsWithin a s → nhdsWithin a (s ∩ t) = nhdsWithin a s
This theorem states that for any type `α` equipped with a topology, and any point `a` and sets `s` and `t` in `α`, if `t` is in the neighborhood within `s` of `a`, then the neighborhood within `s` intersected with `t` of `a` is equal to the neighborhood within `s` of `a`. In simpler terms, if `t` is in the "localized neighborhood" of `a` within `s`, then localizing further by `t` doesn't change the neighborhood within `s` of `a`.
More concisely: For any topological space `(α, τ)`, point `a ∈ α`, and sets `s, t ∈ τ` with `t ∈ Nbd(a, s)`, we have `Nbd(a, s ∩ t) = Nbd(a, s)`.
|
mem_nhdsWithin_of_mem_nhds
theorem mem_nhdsWithin_of_mem_nhds :
∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : Set α} {a : α}, s ∈ nhds a → s ∈ nhdsWithin a t
The theorem states that for any type `α` with a topological space structure, and given two sets `s` and `t` of type `α`, and an element `a` of type `α`, if the set `s` is a neighborhood of `a` (i.e., `s` is in the neighborhood filter of `a`), then `s` is also a neighborhood within `t` of `a` (i.e., `s` is in the "neighborhood within" filter of `a` with respect to `t`). This implies that a neighborhood of `a` remains a neighborhood even when considering the intersection of the neighborhood with another set `t`.
More concisely: Given a topological space `α` and sets `s` and `t` of `α`, if `s` is a neighborhood of an element `a` in `α` and `s` is contained in `t`, then `s` is a neighborhood of `a` within `t`.
|