LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Topology.NhdsSet

`principal_le_nhdsSet` theorem principal_le_nhdsSet : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, Filter.principal s ≤ nhdsSet s The theorem `principal_le_nhdsSet` states that for any given set `s` in a topological space `X`, the principal filter of `s` is less than or equal to the filter of neighborhoods of `s`. In other words, the collection of all supersets of `s` (defined as the principal filter) is a subset of the collection of all neighborhoods of `s` in the topological space `X`. This means every superset of `s` is a neighborhood of `s` in the space `X`. More concisely: For any set $s$ in a topological space $X$, the principal filter of $s$ is contained in the filter of neighborhoods of $s$.
`nhds_le_nhdsSet` theorem nhds_le_nhdsSet : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X} {x : X}, x ∈ s → nhds x ≤ nhdsSet s The theorem `nhds_le_nhdsSet` states that for any type `X` equipped with a topological space structure, any set `s` of type `X`, and any element `x` of type `X`, if `x` belongs to `s`, then the neighborhood filter of `x` (`nhds x`) is less than or equal to the filter of neighborhoods of `s` (`nhdsSet s`). This essentially means that every neighborhood of `x` is also a neighborhood of the set `s`, when `x` is an element of `s`. More concisely: For any topological space (X,τ), set s ∈ X, and x ∈ s, the neighborhood filter of x (nhds x) is contained in the neighborhood filter of s (nhdsSet s).
`monotone_nhdsSet` theorem monotone_nhdsSet : ∀ {X : Type u_1} [inst : TopologicalSpace X], Monotone nhdsSet The theorem `monotone_nhdsSet` states that for any type `X` that comes equipped with a topological space structure, the function `nhdsSet`, which assigns to each set in `X` the filter of its neighborhoods, is monotone. In other words, if we have two sets `A` and `B` in `X` such that `A` is a subset of `B`, then the filter of neighborhoods of `A` is a subset of the filter of neighborhoods of `B`. This is a key property in the study of topological spaces, reflecting the intuitive idea that larger sets have more or "larger" neighborhoods. More concisely: The `nhdsSet` function on a topological space `X`, which maps each set to the filter of its neighborhoods, is monotone with respect to set inclusion.
`eventually_nhdsSet_iff_exists` theorem eventually_nhdsSet_iff_exists : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X} {p : X → Prop}, (∀ᶠ (x : X) in nhdsSet s, p x) ↔ ∃ t, IsOpen t ∧ s ⊆ t ∧ ∀ x ∈ t, p x This theorem states that for any type `X` equipped with a topological space structure, a set `s` of `X`, and a proposition `p` about elements of `X`, the proposition `p` holds true eventually in the neighborhood filter of the set `s` if and only if there exists a larger open set `t` that contains `s` and the proposition `p` holds true for all elements in `t`. In other words, we can say that a property being true "eventually" in the neighborhood of a set `s` is equivalent to the property being true for all elements of a larger open set that contains `s`. This is a fundamental concept in topology and is used to formalize the notion of continuity and limit. More concisely: For any topological space `(X, τ)`, set `s ∈ X`, and proposition `p(x)` on `X`, the proposition `p` holds eventually in the neighborhood filter of `s` if and only if there exists an open set `t ∈ τ` containing `s` such that `p` holds for all `x ∈ t`.
`IsOpen.mem_nhdsSet` theorem IsOpen.mem_nhdsSet : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X}, IsOpen s → (s ∈ nhdsSet t ↔ t ⊆ s) This theorem states that for any type `X` equipped with a topological structure (denoted as `TopologicalSpace X`) and for any two sets `s` and `t` of type `X`, if `s` is an open set, then `s` belongs to the filter of neighborhoods of `t` (denoted as `nhdsSet t`) if and only if `t` is a subset of `s`. In mathematical terms, an open set `s` is in the neighborhood filter of a set `t` precisely when `t` is contained in `s`. More concisely: For any topological space X and sets s and t in X, s is in the neighborhood filter of t if and only if t is a subset of s.
`nhdsSet_mono` theorem nhdsSet_mono : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X}, s ⊆ t → nhdsSet s ≤ nhdsSet t := by sorry This theorem, `nhdsSet_mono`, states that for any type `X` equipped with a topological structure (`TopologicalSpace X`), and for any two sets `s` and `t` of this type, if `s` is a subset of `t` (denoted by `s ⊆ t`), then the filter of neighborhoods of `s` (`nhdsSet s`) is less than or equal to the filter of neighborhoods of `t` (`nhdsSet t`). This is expressed as `nhdsSet s ≤ nhdsSet t`. It means that every neighborhood of `t` contains a neighborhood of `s`, or any set that is "close" to `t` is also "close" to `s`. More concisely: For any topological space `X` and subsets `s` and `t` of `X`, if `s ⊆ t`, then the filter of neighborhoods of `s` is contained in the filter of neighborhoods of `t`.
`mem_nhdsSet_iff_exists` theorem mem_nhdsSet_iff_exists : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X}, s ∈ nhdsSet t ↔ ∃ U, IsOpen U ∧ t ⊆ U ∧ U ⊆ s := by sorry This theorem states that for any two sets `s` and `t` in a given topological space `X`, `s` is in the filter of neighborhoods of `t` if and only if there exists a set `U` such that `U` is open in `X`, `t` is a subset of `U`, and `U` is a subset of `s`. In other words, a set `s` is a neighborhood of another set `t` in the topological space `X` if there's an open set `U` that contains `t` and is contained in `s`. More concisely: A set is a neighborhood of another set in a topological space if and only if it contains an open set that contains the other set.
`nhdsSet_singleton` theorem nhdsSet_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X}, nhdsSet {x} = nhds x This theorem states that for any given topological space `X` and any element `x` of `X`, the filter of neighborhoods of the singleton set containing `x` (`nhdsSet {x}`) is equivalent to the neighborhood filter at `x` (`nhds x`). In other words, the set of all neighborhoods of the singleton set `{x}` is the same as the set of all neighborhoods of the point `x` itself in the topological space `X`. More concisely: For any topological space X and element x ∈ X, the filter of neighborhoods of the singleton set {x} equals the neighborhood filter at x.
`subset_interior_iff_mem_nhdsSet` theorem subset_interior_iff_mem_nhdsSet : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X}, s ⊆ interior t ↔ t ∈ nhdsSet s This theorem is stating that for any topological space `X` and any two sets `s` and `t` of type `X`, `s` is a subset of the interior of `t` if and only if `t` is in the filter of neighborhoods of `s`. In simpler terms, in the context of topology, a set `s` is contained within the largest open subset of `t` if and only if `t` is a neighborhood of `s`. This theorem forms a connection between the concepts of interior of a set and neighborhood filters in a topological space. More concisely: A set is a subset of the interior of another set if and only if the other set is in the filter of neighborhoods of the first set.
`mem_nhdsSet_iff_forall` theorem mem_nhdsSet_iff_forall : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X}, s ∈ nhdsSet t ↔ ∀ x ∈ t, s ∈ nhds x The theorem `mem_nhdsSet_iff_forall` states that for any type `X` that is a topological space and for any two sets `s` and `t` of this type, the set `s` is in the filter of neighborhoods of the set `t` (`nhdsSet t`) if and only if for every element `x` in `t`, the set `s` is in the filter of neighborhoods of `x` (`nhds x`). In other words, a set `s` is a neighborhood of all points in a set `t` if and only if `s` is a neighborhood of each individual point in `t`. More concisely: A set is in the neighborhood filter of a set if and only if it is in the neighborhood filter of each point in that set.
`nhdsSet_union` theorem nhdsSet_union : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s t : Set X), nhdsSet (s ∪ t) = nhdsSet s ⊔ nhdsSet t This theorem states that for any type `X` that is a topological space and any two sets `s` and `t` of type `X`, the filter of neighborhoods of the union of `s` and `t` is equivalent to the join (supremum) of the filter of neighborhoods of `s` and the filter of neighborhoods of `t`. In other words, the set of all neighborhoods of the union of two sets in a topological space is the same as the combined set of all neighborhoods of both sets. More concisely: The filter of neighborhoods of the union of two sets in a topological space is equal to the join (supremum) of the filters of neighborhoods of each set.
`eventually_nhdsSet_iff_forall` theorem eventually_nhdsSet_iff_forall : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X} {p : X → Prop}, (∀ᶠ (x : X) in nhdsSet s, p x) ↔ ∀ x ∈ s, ∀ᶠ (y : X) in nhds x, p y The theorem `eventually_nhdsSet_iff_forall` states that, for any topological space `X`, a set `s` in `X`, and a proposition `p` about elements of `X`, a proposition `p` holds true on a neighborhood filter of the set `s` if and only if the proposition `p` is eventually true near each point in the set `s`. This essentially means that a property is true "locally" around the set `s` if and only if it is true in the "local" neighborhood of each individual point in `s`. The term "eventually true" is used in the context of filters to mean that the property holds for all points sufficiently close to a given point or set. More concisely: A set \(s \subseteq X\) in a topological space \(X\) satisfies the proposition \(p(x)\) for all \(x \in s\) in the neighborhood filter if and only if \(p(x)\) holds eventually in the neighborhood of each \(x \in s\).
`Continuous.tendsto_nhdsSet` theorem Continuous.tendsto_nhdsSet : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {f : X → Y} {t : Set Y}, Continuous f → Set.MapsTo f s t → Filter.Tendsto f (nhdsSet s) (nhdsSet t) This theorem states that for all types `X` and `Y` with topological spaces, and for a set `s` of `X`, a function `f` from `X` to `Y`, and a set `t` of `Y`, if `f` is a continuous function and `f` maps `s` to `t`, then the limit (or the "tendency") of `f` with respect to the neighborhood filter of `s` is less than or equal to the neighborhood filter of `t`. In simpler terms, it means that the preimage of a neighborhood of `t` under a continuous map `f` is a neighborhood of `s` given that `f` maps `s` to `t`. This is a formal way to express a basic principle in topology related to continuous functions and their behavior respect to the concept of neighborhoods. More concisely: For continuous functions between topological spaces, if a function maps a set to another set, then the preimage of a neighborhood of the image under the function is a neighborhood of the set in the domain.
`hasBasis_nhdsSet` theorem hasBasis_nhdsSet : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : Set X), (nhdsSet s).HasBasis (fun U => IsOpen U ∧ s ⊆ U) fun U => U The theorem `hasBasis_nhdsSet` states that for any given type `X` that has a topological space structure and any set `s` of `X`, the filter of neighborhoods of the set `s` (`nhdsSet s`) has a basis consisting of the set of all open sets `U` such that `s` is a subset of `U`. Here, a basis of a filter is a collection of sets that, roughly speaking, generates all other sets in the filter by taking intersections and supersets. More concisely: The filter of neighborhoods of a set in a topological space has a basis consisting of all open sets containing the set.
`IsOpen.nhdsSet_eq` theorem IsOpen.nhdsSet_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsOpen s → nhdsSet s = Filter.principal s This theorem, known as an alias of the reverse direction of `nhdsSet_eq_principal_iff`, states that for any set `s` in a topological space `X`, if `s` is an open set (as defined by `IsOpen`), then the filter of neighborhoods of `s` (as defined by `nhdsSet`) is equal to the principal filter of `s` (as defined by `Filter.principal`). Here, the principal filter of a set is the collection of all its supersets, and the filter of neighborhoods of a set is the supremum over all neighborhoods of the elements of the set in the given topological space. More concisely: If a set `s` in a topological space is open, then its filter of neighborhoods equals its principal filter.
`IsOpen.mem_nhdsSet_self` theorem IsOpen.mem_nhdsSet_self : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsOpen s → s ∈ nhdsSet s This theorem states that for any type `X` with a topological space structure, and for any set `s` of `X`, if `s` is open in this topological space (`IsOpen s`), then `s` is an element of the filter of neighborhoods of `s` (`s ∈ nhdsSet s`). In other words, an open set in a given topological space is always a part of its own filter of neighborhoods. More concisely: In any topological space, every open set is a subset of its own filter of neighborhoods.
`nhdsSet_insert` theorem nhdsSet_insert : ∀ {X : Type u_1} [inst : TopologicalSpace X] (x : X) (s : Set X), nhdsSet (insert x s) = nhds x ⊔ nhdsSet s := by sorry This theorem states that for any type `X` equipped with a topology (which makes `X` a topological space), any element `x` of this type, and any set `s` of elements of this type, the filter of neighborhoods of the set that is the union of `x` and `s` is equal to the join (supremum) of the filter of neighborhoods of `x` and the filter of neighborhoods of the set `s`. In mathematical terms, if `nhdsSet` denotes the filter of neighborhoods and `nhds` the neighborhood filter, we have `nhdsSet (insert x s) = nhds x ⊔ nhdsSet s` for all topological spaces `X`, all `x ∈ X`, and all sets `s` of elements of `X`. More concisely: For any topological space (X, tp), and any x ∈ X and set s ⊆ X, the filter of neighborhoods of the set {x ∪ s} equals the join (supremum) of the filters of neighborhoods of x and s. In mathematical notation, nhds({x ∪ s}) = nhds(x) ⊔ nhds(s).