LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Topology.Basic

`nhds_le_of_le` theorem nhds_le_of_le : ∀ {X : Type u} {x : X} {s : Set X} [inst : TopologicalSpace X] {f : Filter X}, x ∈ s → IsOpen s → Filter.principal s ≤ f → nhds x ≤ f This theorem states that, given any type `X`, any element `x` of `X`, any set `s` of `X`, a topological space structure on `X`, and a filter `f` on `X`, if `x` is an element of `s`, `s` is an open set in the topological space, and the principal filter of `s` is a subfilter of `f` (denoted `Filter.principal s ≤ f`), then the neighborhood filter at `x` is also a subfilter of `f` (denoted `nhds x ≤ f`). In simpler terms, it establishes that to prove a given filter contains the neighborhoods of a point, it is enough to show that it contains all supersets of some open set containing that point. More concisely: Given a topological space `(X, τ)`, if `x ∈ s ∈ τ`, `Filter.principal s ≤ f`, then `nhds x ≤ f`, where `nhds x` is the neighborhood filter at `x`.
`isClosed_compl_iff` theorem isClosed_compl_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsClosed sᶜ ↔ IsOpen s This theorem states that for any type `X` equipped with a topology (represented by the `TopologicalSpace X` instance) and any set `s` of elements of type `X`, the set `s` is closed if and only if its complement `sᶜ` is open. This is a basic property of topological spaces, expressing a deep connection between the notions of open and closed sets. Here, `IsClosed sᶜ` refers to the closedness of the complement of `s`, and `IsOpen s` refers to `s` being an open set in the topological space. More concisely: A set is closed if and only if its complement is open in a topological space.
`interior_empty` theorem interior_empty : ∀ {X : Type u} [inst : TopologicalSpace X], interior ∅ = ∅ This theorem states that for any type `X` which is equipped with a topology (i.e., `X` is a topological space), the interior of the empty set is also the empty set. In mathematical terms, given any topological space `X`, if we consider the set of all open subsets of the empty set that are contained in the empty set itself, the union of all such subsets results in the empty set. This is the definition of the interior of a set in topology. More concisely: The interior of the empty set in a topological space is the empty set.
`continuous_id` theorem continuous_id : ∀ {X : Type u_1} [inst : TopologicalSpace X], Continuous id This theorem states that the identity function is continuous for any topological space. In more formal terms, given any type `X` equipped with a topology (indicated by `TopologicalSpace X`), the identity function (denoted by `id`) on this space is always continuous. Recall that a function is continuous if the preimage of any open set is also an open set. Here, since the identity function just returns its input, it clearly satisfies this property. More concisely: The identity function is continuous on any topological space.
`closure_subset_iff_isClosed` theorem closure_subset_iff_isClosed : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], closure s ⊆ s ↔ IsClosed s This theorem states that for all types `X` and for all sets `s` of type `X` in a given topological space, the closure of `s` is a subset of `s` if and only if `s` is a closed set. In other words, within the constraints of a particular topology, any set `s` is considered closed if and only if every point in its closure is also a point in `s`. More concisely: A set `s` in a topological space is closed if and only if its closure is a subset of `s`.
`Dense.inter_of_isOpen_right` theorem Dense.inter_of_isOpen_right : ∀ {X : Type u} {s t : Set X} [inst : TopologicalSpace X], Dense s → Dense t → IsOpen t → Dense (s ∩ t) The theorem states that in any topological space X, if you have two sets s and t such that both are dense in X, and t is additionally an open set, then the intersection of s and t is also a dense set in X. In other words, every point in the topological space X is either in the intersection of s and t, or is a limit point of this intersection. More concisely: In a topological space X, if sets s and t are dense and open, then their intersection is also a dense set.
`Filter.HasBasis.lift'_interior` theorem Filter.HasBasis.lift'_interior : ∀ {X : Type u} {ι : Sort w} [inst : TopologicalSpace X] {l : Filter X} {p : ι → Prop} {s : ι → Set X}, l.HasBasis p s → (l.lift' interior).HasBasis p fun i => interior (s i) The theorem `Filter.HasBasis.lift'_interior` states that for any type `X`, any type `ι`, and any topological space over `X`, if we have a filter `l` over `X` and two functions `p : ι → Prop` and `s : ι → Set X` such that `l` has a basis defined by the properties `p(i)` and sets `s(i)`, then the filter obtained by lifting `l` via the function `interior` (which assigns to each set its interior) also has a basis defined by the properties `p(i)` and the interiors of the sets `s(i)`. In other words, the interior operation preserves the basis of the filter. More concisely: For any type `X`, topological space over `X`, filter `l` on `X`, and functions `p : ι → Prop` and `s : ι → Set X` such that `l` has a basis given by `p(i)` and `s(i)`, the filter obtained by lifting `l` via the `interior` function also has a basis given by `p(i)` and the interiors of `s(i)`.
`continuous_iff_isClosed` theorem continuous_iff_isClosed : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}, Continuous f ↔ ∀ (s : Set Y), IsClosed s → IsClosed (f ⁻¹' s) This theorem states that a function `f` between two topological spaces `X` and `Y` is continuous if and only if for every closed set `s` in `Y`, the preimage of `s` under `f` is a closed set in `X`. Here, a topological space is a set equipped with a notion of nearness or continuity, the function's preimage of a set is the set of all elements in the domain that map to the elements of that set, and a set is said to be closed if it contains all its limit points. More concisely: A function between two topological spaces is continuous if and for every closed set in the codomain, its preimage is a closed set in the domain.
`ClusterPt.mono` theorem ClusterPt.mono : ∀ {X : Type u} {x : X} [inst : TopologicalSpace X] {f g : Filter X}, ClusterPt x f → f ≤ g → ClusterPt x g := by sorry The theorem `ClusterPt.mono` states that for any type `X` equipped with a topology, any point `x` in `X`, and any two filters `f` and `g` on `X`, if `x` is a cluster point of the filter `f` and `f` is a subfilter of `g` (i.e., `f` is contained within `g`), then `x` is also a cluster point of the filter `g`. Here, a cluster point of a filter `F` on `X` is defined to be a point `x` in `X` such that the intersection of the neighborhood filter of `x` and `F` is not the trivial (or bottom) filter. In simpler terms, the theorem is saying that if a point is close to many points of a certain collection (represented by filter `f`), and that collection is a part of a larger collection (represented by filter `g`), then the point is also close to many points of the larger collection. More concisely: If a filter `f` is a subfilter of filter `g` on a topological space `X`, and a point `x` in `X` is a cluster point of `f`, then `x` is also a cluster point of `g`.
`tendsto_nhds` theorem tendsto_nhds : ∀ {X : Type u} {α : Type u_1} {x : X} [inst : TopologicalSpace X] {f : α → X} {l : Filter α}, Filter.Tendsto f l (nhds x) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → f ⁻¹' s ∈ l This theorem, `tendsto_nhds`, states a condition for a function to tend towards a limit in a topological space. Specifically, for a given type `X` with a topological space structure, a function `f` from some type `α` to `X`, a point `x` from `X`, and a filter `l` on `α`, the function `f` tends towards `x` (represented by `Filter.Tendsto f l (nhds x)`) if and only if for every set `s` of type `X` that is open and contains `x`, the preimage of `s` under `f` belongs to the filter `l`. Here, the preimage of `s` under `f` (`f ⁻¹' s`) is the set of elements in `α` that `f` maps into `s`. This theorem provides a characterization of the limit of a function in terms of open sets and their pre-images under the function. More concisely: A function from a type to a topological space tends towards a limit point if and only if the preimage of every open neighborhood of the limit point is in the filter.
`mem_interior_iff_mem_nhds` theorem mem_interior_iff_mem_nhds : ∀ {X : Type u} {x : X} {s : Set X} [inst : TopologicalSpace X], x ∈ interior s ↔ s ∈ nhds x This theorem states that for any type `X`, any element `x` of `X`, and any set `s` of `X`, given that `X` has a topological space structure, `x` is in the interior of `s` if and only if `s` is in the neighborhood of `x`. In more mathematical terms, it's stating that an element `x` belongs to the interior of a set `s` (which is the largest open subset of `s`) if and only if the set `s` is a neighborhood of `x` (i.e., it contains an open set around `x`). This theorem is a key result in topology, relating the notions of interior of a set and neighborhood filter of a point. More concisely: For any topological space (X,τ), element x ∈ X, and set s ∈ τ, x belongs to the interior of s if and only if s is a neighborhood of x.
`Mathlib.Topology.Basic._auxLemma.62` theorem Mathlib.Topology.Basic._auxLemma.62 : ∀ {X : Type u} {x : X} {s : Set X} [inst : TopologicalSpace X], (x ∈ closure s) = ∀ t ∈ nhds x, (t ∩ s).Nonempty This theorem states that for any type `X`, any element `x` of `X`, and any set `s` of `X`, in the context of a topological space over `X`, the element `x` is in the closure of the set `s` if and only if for every neighborhood `t` of `x`, the intersection of `t` and `s` is not empty. In other words, a point belongs to the closure of a set if every neighborhood of that point intersects the set. More concisely: A point `x` in a topological space lies in the closure of a set `s` if and only if for every neighborhood `t` of `x`, the intersection `t ∩ s` is non-empty.
`mem_closure_iff_nhds_basis'` theorem mem_closure_iff_nhds_basis' : ∀ {X : Type u} {ι : Sort w} {x : X} {t : Set X} [inst : TopologicalSpace X] {p : ι → Prop} {s : ι → Set X}, (nhds x).HasBasis p s → (x ∈ closure t ↔ ∀ (i : ι), p i → (s i ∩ t).Nonempty) The theorem `mem_closure_iff_nhds_basis'` states that for any type `X`, subset `t` of `X`, element `x` of `X`, and a topology on `X`, along with a basis `s` indexed by `ι` for the neighborhood filter of `x` such that each set in the basis satisfies some property `p`, the element `x` is in the closure of the set `t` if and only if for all `i` in `ι` where `p i` holds, the intersection of `s i` and `t` is not empty. In simpler terms, a point is in the closure of a set if every neighborhood of the point intersects the set, considering neighborhoods from a specific basis that satisfy a certain property. More concisely: For any topological space $(X, \tau)$, subset $t \subseteq X$, point $x \in X$, and basis $s: \ι \to \mathcal{P}(X)$ for the neighborhood filter of $x$ such that each $s(i) \in \tau$ satisfies property $p$, $x \in \overline{t}$ if and only if for all $i \in \ι$ with $p(i)$, $s(i) \cap t \neq \emptyset$.
`closure_compl` theorem closure_compl : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], closure sᶜ = (interior s)ᶜ This theorem states that, for any set `s` in a topological space `X`, the closure of the complement of `s` is equal to the complement of the interior of `s`. In other words, it provides a relationship between the complementary operations and the closure and interior operations in a topological space. The closure of a set `s` represents the smallest closed set that includes `s`, while the interior of `s` represents the largest open set that is a subset of `s`. The complement of a set is the set of all elements not in the set, so this theorem shows how these concepts interact. More concisely: The closure of a set's complement is equal to the complement of its interior in a topological space.
`Set.Finite.isClosed_biUnion` theorem Set.Finite.isClosed_biUnion : ∀ {X : Type u} {α : Type u_1} [inst : TopologicalSpace X] {s : Set α} {f : α → Set X}, s.Finite → (∀ i ∈ s, IsClosed (f i)) → IsClosed (⋃ i ∈ s, f i) This theorem states that for any type `X` equipped with a topology (i.e., `X` is a topological space) and any type `α`, if `s` is a finite set of elements of type `α` and `f` is a function from `α` to the set of subsets of `X`, then if every subset `f(i)` where `i` is an element of `s` is closed, the union of all such subsets `f(i)` for `i` in `s` is also closed. In simpler terms, it says that the union of a finite collection of closed sets in a topological space is itself a closed set. More concisely: In a topological space, the union of a finite number of closed sets is closed.
`pure_le_nhds` theorem pure_le_nhds : ∀ {X : Type u} [inst : TopologicalSpace X], pure ≤ nhds This theorem states that for any type `X` endowed with a topology (i.e., `X` is a topological space), the pure filter is less than or equal to the neighborhood filter. In mathematical terms, for every point in the topological space `X`, the principal filter generated by that point is contained within the collection of all neighborhoods of that point. More concisely: For every point in a topological space, the principal filter generated by that point is contained in the neighborhood filter.
`mem_closure_iff_nhds_basis` theorem mem_closure_iff_nhds_basis : ∀ {X : Type u} {ι : Sort w} {x : X} {t : Set X} [inst : TopologicalSpace X] {p : ι → Prop} {s : ι → Set X}, (nhds x).HasBasis p s → (x ∈ closure t ↔ ∀ (i : ι), p i → ∃ y ∈ t, y ∈ s i) This theorem, `mem_closure_iff_nhds_basis`, states that for any topological space `X`, an indexing type `ι`, a point `x` in `X`, and a set `t` of `X`, given a basis `{s i \| p i}` for the neighborhood filter at `x`, then `x` is a member of the closure of `t` if and only if for all `i` in `ι` such that `p i` is true, there exists an element `y` in `t` that is also in `s i`. Here, the basis of a filter is a system of sets that can be used to generate the entire filter, and the closure of a set `t` is the smallest closed set that contains `t`. Essentially, the theorem establishes a condition for when a point is in the closure of a set, in terms of the basis sets of the point's neighborhood filter. More concisely: For any topological space X, point x in X, set t, and basis {si : p i} for the neighborhood filter at x, x is in the closure of t if and only if for all i, if p i then there exists y in t with y in si.
`ContinuousAt.preimage_mem_nhds` theorem ContinuousAt.preimage_mem_nhds : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {x : X} {t : Set Y}, ContinuousAt f x → t ∈ nhds (f x) → f ⁻¹' t ∈ nhds x This theorem, `ContinuousAt.preimage_mem_nhds`, states that for all types `X` and `Y` with the structure of topological spaces, any function `f` from `X` to `Y`, and any point `x` in `X` and set `t` of `Y`, if `f` is continuous at `x` and `t` is a neighborhood of `f(x)`, then the preimage of `t` under `f` is a neighborhood of `x`. In other words, the preimage of any neighborhood of `f(x)` under a function `f` that is continuous at `x`, forms a neighborhood of `x` in `X`. More concisely: For all topological spaces X and Y, continuous function f : X -> Y, point x in X, and neighborhood t of f(x) in Y, the preimage f^(-1)(t) is a neighborhood of x in X.
`DenseRange.nonempty_iff` theorem DenseRange.nonempty_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {α : Type u_4} {f : α → X}, DenseRange f → (Nonempty α ↔ Nonempty X) The theorem `DenseRange.nonempty_iff` states that for any two types `X` and `α`, given `X` has a topology structure and `f` is a function from `α` to `X`, if `f` has a dense range, then `α` is nonempty if and only if `X` is nonempty. This is to say, there exists an element in `α` if and only if there exists an element in `X`, given the range of `f` is dense in `X`. More concisely: A function from a nonempty type to a nonempty topological space with a dense range has a nonempty domain.
`interior_univ` theorem interior_univ : ∀ {X : Type u} [inst : TopologicalSpace X], interior Set.univ = Set.univ The theorem `interior_univ` states that for all types `X` which have a topology defined on them, the interior of the universal set is equal to the universal set itself. In simpler terms, it says that the largest open subset of the set containing all elements is the set of all elements itself. This is true for any type `X` and any topological space `X`. In standard mathematical notation, if `X` is a topological space, then `interior(X) = X`. More concisely: For any topological space X, the interior of the universal set X is equal to X.
`eventually_nhds_iff` theorem eventually_nhds_iff : ∀ {X : Type u} {x : X} [inst : TopologicalSpace X] {p : X → Prop}, (∀ᶠ (x : X) in nhds x, p x) ↔ ∃ t, (∀ x ∈ t, p x) ∧ IsOpen t ∧ x ∈ t This theorem states that a predicate is true in a neighborhood of a point 'x' if and only if it is true for all the points in an open set containing 'x'. In other words, for a given topological space 'X', a point 'x' in 'X', and a predicate 'p' on 'X', the property 'p' holds eventually (i.e., in the neighborhood filter) at 'x' if and only if there exists an open set 't' containing 'x' such that 'p' holds for every point in 't'. More concisely: A predicate holds in a neighborhood of a point if and only if it holds in every point of some open set containing that point.
`Disjoint.closure_left` theorem Disjoint.closure_left : ∀ {X : Type u} {s t : Set X} [inst : TopologicalSpace X], Disjoint s t → IsOpen t → Disjoint (closure s) t := by sorry This theorem states that for any type `X` with a defined `TopologicalSpace`, and for any two sets `s` and `t` of this type, if `s` and `t` are disjoint and `t` is an open set in this topological space, then the closure of `s` is also disjoint from `t`. In other words, in a given topological context, if two sets do not share any common elements and one of them is open, then the smallest closed set that contains one of those sets will still not share any common elements with the other set. More concisely: If two disjoint sets in a topological space have one of them open, then their closures are still disjoint.
`isOpen_biUnion` theorem isOpen_biUnion : ∀ {X : Type u} {α : Type u_1} [inst : TopologicalSpace X] {s : Set α} {f : α → Set X}, (∀ i ∈ s, IsOpen (f i)) → IsOpen (⋃ i ∈ s, f i) The theorem `isOpen_biUnion` states that for any type `X` with a topological space structure, a set `s` of another type `α`, and a function `f` from `α` to sets of `X`, if for all elements (`i`) in the set `s`, the set `f(i)` is open, then the union of all the sets `f(i)` (for `i` in `s`) is also open. In other words, it's saying that the union of an arbitrary collection of open sets is also an open set. More concisely: If every set in an arbitrary collection is open in a topological space, then their union is also open.
`Dense.inter_nhds_nonempty` theorem Dense.inter_nhds_nonempty : ∀ {X : Type u} {x : X} {s t : Set X} [inst : TopologicalSpace X], Dense s → t ∈ nhds x → (s ∩ t).Nonempty := by sorry This theorem states that for any type `X` equipped with a topological space structure, for any point `x` in `X`, and for any sets `s` and `t` in `X`, if `s` is a dense set and `t` is a neighborhood of `x`, then the intersection of `s` and `t` is nonempty. In other words, there is at least one element of `X` that belongs to both the dense set `s` and the neighborhood `t` of `x`. More concisely: For any topological space `(X,τ)` and point `x ∈ X`, if `s ⊆ X` is dense and `t ∈ β(x)` is a neighborhood of `x`, then `s ∩ t ≠ ∅`.
`interior_singleton` theorem interior_singleton : ∀ {X : Type u} [inst : TopologicalSpace X] (x : X) [inst_1 : (nhdsWithin x {x}ᶜ).NeBot], interior {x} = ∅ := by sorry The theorem `interior_singleton` states that for any point `x` in a topological space `X`, if `x` is not an isolated point (meaning it is not alone in its own neighborhood), then the interior of the set containing only `x` is empty. In other words, there are no open sets within the set `{x}` that are contained entirely within `{x}`, as would be expected if `x` is not an isolated point. This is expressed in terms of the "neighborhood within" filter: if the intersection of the complement of `{x}` and any neighborhood of `x` is non-empty (`nhdsWithin x {x}ᶜ` is not a bottom element), then `x` is not an isolated point. More concisely: If a point in a topological space is not isolated, then the interior of the set containing only that point is empty.
`mem_closure_of_tendsto` theorem mem_closure_of_tendsto : ∀ {X : Type u} {α : Type u_1} {x : X} {s : Set X} [inst : TopologicalSpace X] {f : α → X} {b : Filter α} [inst_1 : b.NeBot], Filter.Tendsto f b (nhds x) → (∀ᶠ (x : α) in b, f x ∈ s) → x ∈ closure s This theorem states that, given a type `X` equipped with a topological space structure, a type `α`, an element `x` of `X`, a set `s` of `X`, a function `f` from `α` to `X`, and a filter `b` on `α` which is not the bottom filter, if the function `f` tends from filter `b` to the neighborhood filter of `x` and almost every element `x` in the filter `b` is in the set `s` when mapped under function `f`, then `x` is in the closure of the set `s` in the topology of `X`. In other words, if a function satisfies these conditions, then the limit point of the function belongs to the closure of the set through which almost all points in the filter pass under the function. More concisely: If a function from a non-bottom filter on a space equipped with a topology maps almost all filter elements to a set and tends to a limit point in the neighborhood of a point in the space, then that limit point is in the closure of the set in the topology.
`Mathlib.Topology.Basic._auxLemma.1` theorem Mathlib.Topology.Basic._auxLemma.1 : ∀ {X : Type u} [inst : TopologicalSpace X], IsOpen ∅ = True This theorem states that for any type `X` equipped with a topology (meaning it is an instance of a topological space), the empty set is always an open set in this topological space. This property is universal and does not depend on the specifics of the topological space under consideration. More concisely: In any topological space, the empty set is open.
`isClosed_biInter` theorem isClosed_biInter : ∀ {X : Type u} {α : Type u_1} [inst : TopologicalSpace X] {s : Set α} {f : α → Set X}, (∀ i ∈ s, IsClosed (f i)) → IsClosed (⋂ i ∈ s, f i) This theorem states that for any types `X` and `α`, given a topological space on `X`, a set `s` of elements of type `α`, and a function `f` from `α` to a set of `X`, if every set `f i` where `i` belongs to `s` is closed in the topological sense, then the intersection of all such sets `f i` is also a closed set. In other words, the intersection of an arbitrary collection of closed sets, indexed by a set `s`, remains closed. More concisely: Given a topological space `X`, any family of closed subsets `{f(i) \| i ∈ s}`, where `s` is a set and `f : α -> X` is a function from a type `α` to `X`, their intersection is closed in `X`.
`DenseRange.subset_closure_image_preimage_of_isOpen` theorem DenseRange.subset_closure_image_preimage_of_isOpen : ∀ {X : Type u_1} [inst : TopologicalSpace X] {α : Type u_4} {f : α → X} {s : Set X}, DenseRange f → IsOpen s → s ⊆ closure (f '' (f ⁻¹' s)) The theorem `DenseRange.subset_closure_image_preimage_of_isOpen` states that for any type `X` with a given topological space structure, any type `α`, any function `f` from `α` to `X`, and any set `s` in `X`, if `f` has a dense range and `s` is an open set in the codomain of `f`, then `s` is a subset of the closure of the image of the preimage of `s` under `f`. In other words, if `f` densely covers `X` and `s` is an open set in `X`, then every point in `s` is either in the image of `f` applied to the preimage of `s`, or can be approximated by such points; thus, the image of the preimage of `s` under `f` is dense in `s`. More concisely: If `f: α → X` is a dense function with open codomain subset `s ∈ X` of the range of `f`, then `s ⊆ closure (image (preimage s f))`.
`mem_closure_iff_nhds` theorem mem_closure_iff_nhds : ∀ {X : Type u} {x : X} {s : Set X} [inst : TopologicalSpace X], x ∈ closure s ↔ ∀ t ∈ nhds x, (t ∩ s).Nonempty := by sorry The theorem `mem_closure_iff_nhds` states that for any type `X`, any element `x` of `X`, and any set `s` of `X` in a topological space, `x` is in the closure of `s` if and only if for every set `t` in the neighborhood of `x`, the intersection of `t` and `s` is not empty. In other words, a point is in the closure of a set if and only if every neighborhood of that point intersects the set. More concisely: A point x is in the closure of a set s in a topological space if and only if for every neighborhood t of x, the intersection of t and s is non-empty.
`Continuous.tendsto'` theorem Continuous.tendsto' : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}, Continuous f → ∀ (x : X) (y : Y), f x = y → Filter.Tendsto f (nhds x) (nhds y) This theorem, `Continuous.tendsto'`, states that for any types `X` and `Y` equipped with topological spaces and any function `f : X → Y` that is continuous, if `y` is the value of `f` at `x`, then the function `f` tends to `y` as `x` tends to its neighborhood. In other words, for every neighborhood of `y`, the preimage under `f` is a neighborhood of `x`. This is a more specific form of the `Continuous.tendsto` theorem that allows for a simpler way to specify the limit of a function at a point. For example, it enables the expression `continuous_exp.tendsto' 0 1 exp_zero` to describe the limit of the exponential function at point 0 is 1. More concisely: Given types `X` and `Y` with topological spaces, and a continuous function `f : X → Y`: for every neighborhood `V` of `y` in `Y`, there exists a neighborhood `U` of `x` in `X` such that `f(U) ⊆ V`.
`interior_subset` theorem interior_subset : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], interior s ⊆ s This theorem states that for any given type `X` and a set `s` of `X` type, in the context of a topological space defined on `X`, the interior of the set `s` is always a subset of `s`. In other words, in any topological space, the interior of any set is contained within the set itself. More concisely: In any topological space, the interior of a set is a subset of the set itself.
`all_mem_nhds_filter` theorem all_mem_nhds_filter : ∀ {X : Type u} {α : Type u_1} [inst : TopologicalSpace X] (x : X) (f : Set X → Set α), (∀ (s t : Set X), s ⊆ t → f s ⊆ f t) → ∀ (l : Filter α), (∀ s ∈ nhds x, f s ∈ l) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → f s ∈ l This theorem states that for any topological space `X` and any type `α`, given any point `x` in `X` and a function `f` from the sets of `X` to the sets of `α`, where `f` respects set inclusion in the sense that if one set `s` is a subset of another set `t`, then `f(s)` is a subset of `f(t)`. Then for any filter `l` of `α`, the condition that for each neighborhood `s` of `x`, `f(s)` belongs to `l` is equivalent to the condition that for each open set `s` containing `x`, `f(s)` belongs to `l`. In other words, whether you take the neighborhood around `x` or any open set containing `x`, the image of this set under `f` is always in the filter `l` whenever the function `f` respects set inclusion. More concisely: For any topological space X and type α, if function f from subsets of X to subsets of α respects set inclusion and x is a point in X, then the filter l of α contains the image of every neighborhood of x if and only if it contains the image of every open set containing x.
`closure_empty` theorem closure_empty : ∀ {X : Type u} [inst : TopologicalSpace X], closure ∅ = ∅ This theorem states that for any type `X` that forms a topological space, the closure of the empty set is also the empty set. In other words, the smallest closed set that contains the empty set, in the context of any given topological space, is the empty set itself. More concisely: In any topological space, the closure of the empty set is the empty set.
`closure_nonempty_iff` theorem closure_nonempty_iff : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], (closure s).Nonempty ↔ s.Nonempty This theorem, `closure_nonempty_iff`, establishes a relationship between a set and its closure in the context of a topological space. Specifically, it states that for any set `s` in a topological space `X`, the closure of `s` is nonempty if and only if `s` itself is nonempty. In mathematical terms, this means there exists an element in `s` if and only if there exists an element in the closure of `s`. More concisely: The closure of a non-empty set in a topological space is non-empty. Equivalently, a set is non-empty if and only if its closure is non-empty.
`Set.Finite.isOpen_sInter` theorem Set.Finite.isOpen_sInter : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set (Set X)}, s.Finite → (∀ t ∈ s, IsOpen t) → IsOpen s.sInter := by sorry The theorem `Set.Finite.isOpen_sInter` states that for any type `X` with a topological space structure, and for any set `s` which is a set of sets of `X`, if `s` is finite and each set `t` within `s` is open in the topological space, then the intersection of all sets in `s` (denoted by `⋂₀ s`) is also open in the topological space. In other words, the intersection of a finite collection of open sets in a topological space is also an open set. More concisely: The intersection of a finite number of open sets in a topological space is open.
`TopologicalSpace.ext` theorem TopologicalSpace.ext : ∀ {X : Type u} {f g : TopologicalSpace X}, IsOpen = IsOpen → f = g This theorem, `TopologicalSpace.ext`, asserts that for any type `X`, if two topological spaces `f` and `g` over `X` have the property that their `IsOpen` predicates are the same, then `f` and `g` must be identical. In other words, a topological space is uniquely determined by its open sets. More concisely: If two topological spaces over a type `X` have identical open sets, then they are equal.
`IsClosed.mem_of_frequently_of_tendsto` theorem IsClosed.mem_of_frequently_of_tendsto : ∀ {X : Type u} {α : Type u_1} {x : X} {s : Set X} [inst : TopologicalSpace X] {f : α → X} {b : Filter α}, IsClosed s → (∃ᶠ (x : α) in b, f x ∈ s) → Filter.Tendsto f b (nhds x) → x ∈ s This theorem states that for any type `X` and `α`, and given a set `s` of type `X` and a function `f` from `α` to `X`, if `s` is a closed set in a topological space, and if there are frequently (meaning on a set of elements whose complement has empty interior) elements of `b`, a filter on `α`, such that their images under `f` belong to `s`, and if the function `f` tends to a limit which lies in the neighborhood filter at a point `x` in `X` when evaluated at points from `b`, then `x` is an element of `s`. In essence, it says that if a function's range frequently lies in a closed set and the function tends to a limit, then that limit point belongs to the closed set. More concisely: If a closed set `s` in a topological space and a function `f` from `α` to `X` have the property that for some filter `b` on `α`, the images of elements in `b` under `f` lie in `s` and `f` converges to a limit in `s` at a point `x` in `X`, then `x` is an element of `s`.
`continuous_const` theorem continuous_const : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {y : Y}, Continuous fun x => y This theorem states that for any two types `X` and `Y`, where `X` and `Y` are endowed with a topological structure (i.e., `X` and `Y` are topological spaces), any function that maps every element of `X` to a specific constant element `y` of `Y` is continuous. In the language of mathematics, it means a constant function between two topological spaces is always continuous. More concisely: Given any two topological spaces `X` and `Y`, and any constant function `f : X → Y`, the function `f` is continuous.
`frontier_eq_closure_inter_closure` theorem frontier_eq_closure_inter_closure : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], frontier s = closure s ∩ closure sᶜ This theorem states that for any set `s` within a topological space `X`, the frontier of `s` is equal to the intersection of the closure of `s` and the closure of the complement of `s`. In the context of topology, the frontier of a set is defined as the set of points that lie between the closure and the interior of the set. The closure of a set is the smallest closed set containing the set, and the complement of a set is a set of all points not in the original set. Hence, this theorem precisely defines the frontier in terms of these other fundamental operations in topology. More concisely: The frontier of a set in a topological space is equal to the intersection of its closure and the closure of its complement.
`accPt_iff_nhds` theorem accPt_iff_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] (x : X) (C : Set X), AccPt x (Filter.principal C) ↔ ∀ U ∈ nhds x, ∃ y ∈ U ∩ C, y ≠ x The theorem `accPt_iff_nhds` states that for any type `X` equipped with a topology and any element `x` of `X` and a set `C` of elements of `X`, `x` is an accumulation point of the set `C` if and only if every neighborhood of `x` contains a point of `C` that is not equal to `x`. Here, a neighborhood of `x` is a set that contains an open set around `x`, and an accumulation point of a set `C` is a point such that every neighborhood of this point intersects with `C` at a point different from the accumulation point itself. More concisely: A point x in a topological space X is an accumulation point of a set C if and only if for every neighborhood of x, there exists a point y in C different from x that belongs to that neighborhood.
`mem_nhds_iff` theorem mem_nhds_iff : ∀ {X : Type u} {x : X} {s : Set X} [inst : TopologicalSpace X], s ∈ nhds x ↔ ∃ t ⊆ s, IsOpen t ∧ x ∈ t This theorem states that for any type `X`, any point `x` of type `X`, and any set `s` of type `Set X` in a given topological space, `s` is a neighborhood of `x` (i.e., `s` is in the neighborhood filter of `x`, represented as `s ∈ nhds x`) if and only if there exists a set `t` such that `t` is a subset of `s` (`t ⊆ s`), `t` is an open set (`IsOpen t`), and `x` is an element of `t` (`x ∈ t`). In more informal terms, a set is a neighborhood of a point in a topological space if and only if it contains an open set in which the point resides. More concisely: In a topological space, a set is a neighborhood of a point if and only if it contains an open set that includes the point.
`IsOpen.subset_interior_iff` theorem IsOpen.subset_interior_iff : ∀ {X : Type u} {s t : Set X} [inst : TopologicalSpace X], IsOpen s → (s ⊆ interior t ↔ s ⊆ t) The theorem `IsOpen.subset_interior_iff` states that for any type `X` and any two sets `s` and `t` of type `X` in a given topological space, if `s` is an open set, then `s` is a subset of the interior of `t` if and only if `s` is a subset of `t`. In other words, for an open set `s`, being a subset of the interior of `t` is equivalent to being a subset of `t` itself. More concisely: An open set is a subset of the interior of another set if and only if it is a subset of that set.
`mem_closure_iff_ultrafilter` theorem mem_closure_iff_ultrafilter : ∀ {X : Type u} {x : X} {s : Set X} [inst : TopologicalSpace X], x ∈ closure s ↔ ∃ u, s ∈ u ∧ ↑u ≤ nhds x The theorem `mem_closure_iff_ultrafilter` states that for any type `X`, point `x` of type `X`, and a set `s` of type `X` in a topological space, `x` belongs to the closure of `s` if and only if there exists some ultrafilter `u` such that `s` is in `u` and `u` converges to `x` in the neighborhood filter at `x`. In other words, a point is in the closure of a set if and only if there is an ultrafilter on the set that converges to the point. More concisely: A point belongs to the closure of a set in a topological space if and only if there exists an ultrafilter on the set converging to that point.
`Continuous.closure_preimage_subset` theorem Continuous.closure_preimage_subset : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}, Continuous f → ∀ (t : Set Y), closure (f ⁻¹' t) ⊆ f ⁻¹' closure t This theorem states that for any types `X` and `Y` with respective topological spaces, and for any function `f` from `X` to `Y` that is continuous, the closure of the preimage of a set `t` under `f` is a subset of the preimage of the closure of `t` under `f`. In simpler terms, if you take a set `t` in `Y`, find its preimage in `X`, and then take the closure of that preimage, you end up with a set that is entirely contained within the preimage of the closure of `t`. It's a statement about how continuous functions interact with the process of taking closures and preimages in topological spaces. More concisely: For any continuous function $f$ from a topological space $X$ to a topological space $Y$ and any set $t$ in $Y$, the closure of $f^{-1}(t)$ is contained in $f^{-1}(\overline{t})$.
`nhds_basis_opens'` theorem nhds_basis_opens' : ∀ {X : Type u} [inst : TopologicalSpace X] (x : X), (nhds x).HasBasis (fun s => s ∈ nhds x ∧ IsOpen s) fun x => x The theorem `nhds_basis_opens'` states that for any topological space `X` and any point `x` in `X`, the open neighborhoods of `x` constitute a basis for the neighborhood filter of `x`. This basis is defined by the property that a set is in the neighborhood of `x` and is an open set. In mathematical terms, the filter of neighborhoods at a point `x` is generated by the collection of all open neighborhoods of `x`. More concisely: The collection of open neighborhoods of a point `x` in a topological space forms a basis for the neighborhood filter of `x`.
`closure_eq_compl_interior_compl` theorem closure_eq_compl_interior_compl : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], closure s = (interior sᶜ)ᶜ This theorem states that for any type `X`, any `s` which is a set of `X`, and given that `X` is a topological space, the closure of the set `s` is equal to the complement of the interior of the complement of `s`. In other words, it says that in any topological space, the closure of a set is the same as taking the set, finding its complement (all points not in the set), determining the interior of that complement, and then taking the complement of that interior. More concisely: In a topological space, the closure of a set is equal to the complement of the interior of its complement.
`continuous_iff_ultrafilter` theorem continuous_iff_ultrafilter : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}, Continuous f ↔ ∀ (x : X) (g : Ultrafilter X), ↑g ≤ nhds x → Filter.Tendsto f (↑g) (nhds (f x)) This theorem, named `continuous_iff_ultrafilter`, states that a function `f` between two topological spaces `X` and `Y` is continuous if and only if for every element `x` in `X` and any ultrafilter `g` on `X` such that `g` is included in the neighborhood of `x`, the image of `g` under `f` converges to the image of `x` under `f`. In other words, the function `f` preserves the convergence of ultrafilters. More concisely: A function between topological spaces is continuous if and only if it preserves the convergence of ultrafilters, that is, for every ultrafilter on the domain and every point in its base, the image of the ultrafilter converges to the image of that point under the function.
`isClosed_setOf_clusterPt` theorem isClosed_setOf_clusterPt : ∀ {X : Type u} [inst : TopologicalSpace X] {f : Filter X}, IsClosed {x \| ClusterPt x f} This theorem states that the set of all cluster points of a given filter is a closed set. In the context of topological spaces, a closed set is one that contains all its limit points. In particular, this property also applies to sequences, implying that the set of all limit points of a sequence is a closed set. In mathematical notation, if `X` is a type and `f` is a filter on `X`, then the set `{x : X \| ClusterPt x f}` is closed, where `ClusterPt` indicates that `x` is a cluster point of filter `f`. More concisely: The set of cluster points of a filter is a closed set in the sense that it contains all its limit points.
`DenseRange.dense_image` theorem DenseRange.dense_image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {f : X → Y}, DenseRange f → Continuous f → Dense s → Dense (f '' s) The theorem `DenseRange.dense_image` asserts that, for any two topological spaces `X` and `Y` and a function `f` from `X` to `Y`, if `f` has dense range (meaning the set of its output values is dense in `Y`) and `f` is continuous, and if a set `s` in `X` is dense, then the image of `s` under `f` (denoted as `f '' s`) is also dense in `Y`. In other words, applying a continuous function with dense range to a dense set preserves the property of being dense. More concisely: If a continuous function with dense range maps a dense subset to a subset with the same density property in its domain.
`mem_of_mem_nhds` theorem mem_of_mem_nhds : ∀ {X : Type u} {x : X} {s : Set X} [inst : TopologicalSpace X], s ∈ nhds x → x ∈ s This theorem states that for any type `X`, any element `x` of this type, and any set `s` of elements of type `X`, given that `X` is a topological space, if `s` is a neighborhood of `x` (i.e., `s` is in the neighborhood filter of `x`), then `x` belongs to the set `s`. In other words, any point is a member of every one of its neighborhoods in a given topological space. More concisely: In a topological space, any point is contained in every neighborhood of that point.
`clusterPt_principal_iff` theorem clusterPt_principal_iff : ∀ {X : Type u} {x : X} {s : Set X} [inst : TopologicalSpace X], ClusterPt x (Filter.principal s) ↔ ∀ U ∈ nhds x, (U ∩ s).Nonempty The theorem `clusterPt_principal_iff` states that for any type `X`, any element `x` of `X`, and any set `s` of `X` within a topological space, `x` is a cluster point of the set `s` if and only if every neighborhood `U` of `x` has a nonempty intersection with `s`. In other words, `x` is a cluster point of `s` if there is at least one point from `s` in every neighborhood of `x`. A neighborhood of `x` is a set that contains an open set around `x`. This theorem provides a characterization of cluster points in terms of neighborhoods and their intersections with the given set `s`. More concisely: A point x in a topological space is a cluster point of a set s if and only if for every neighborhood U of x, s intersects U is nonempty.
`IsClosed.preimage` theorem IsClosed.preimage : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}, Continuous f → ∀ {t : Set Y}, IsClosed t → IsClosed (f ⁻¹' t) This theorem states that, given two types `X` and `Y` each equipped with a topological structure (represented by `TopologicalSpace X` and `TopologicalSpace Y` respectively), for any function `f` from `X` to `Y` that is continuous, if a set `t` in `Y` is closed (denoted by `IsClosed t`), then the preimage of `t` under `f` is also closed in `X` (where `f ⁻¹' t` denotes the preimage of `t` under `f`). In other words, continuous functions map closed sets to closed sets under the operation of taking preimages. More concisely: If `f` is a continuous function between topological spaces `X` and `Y`, and `t` is a closed set in `Y`, then the preimage `f ⁻¹' t` is a closed set in `X`.
`Set.Finite.interior_biInter` theorem Set.Finite.interior_biInter : ∀ {X : Type u} [inst : TopologicalSpace X] {ι : Type u_3} {s : Set ι}, s.Finite → ∀ (f : ι → Set X), interior (⋂ i ∈ s, f i) = ⋂ i ∈ s, interior (f i) This theorem, `Set.Finite.interior_biInter`, states that for any type `X` that is a topological space, any type `ι`, and any set `s` of type `ι`, if `s` is finite, then for any function `f` from `ι` to the set of `X`, the interior of the intersection of the sets `f i` for each `i` in `s` is equal to the intersection of the interiors of the sets `f i` for each `i` in `s`. In other words, if we have a finite index set and a function mapping each index to a set in a topological space, then the interior of the intersection of these sets can be found by first finding the interior of each individual set and then finding the intersection of these interiors. More concisely: For any topological space X, finite index set ι, and function f from ι to the powerset of X, the interior of ∩ (fi : i ∈ ι) equals ∧ (int (fi) : i ∈ ι).
`ContinuousAt.comp` theorem ContinuousAt.comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z] {f : X → Y} {x : X} {g : Y → Z}, ContinuousAt g (f x) → ContinuousAt f x → ContinuousAt (g ∘ f) x The theorem `ContinuousAt.comp` states that for three given types `X`, `Y`, and `Z` each equipped with a topological structure, if `f` is a function from `X` to `Y` and `g` is a function from `Y` to `Z`, and if `f` is continuous at a point `x` in `X` and `g` is continuous at the point `f(x)` in `Y`, then the composition of `g` and `f`, denoted by `g ∘ f`, is continuous at the point `x` in `X`. In terms of mathematics, this theorem is essentially the statement of the composition of continuous functions being continuous. More concisely: If functions $f : X \rightarrow Y$ and $g : Y \rightarrow Z$ are continuous at points $x \in X$ and $y = f(x) \in Y$, respectively, then their composition $g \circ f : X \rightarrow Z$ is continuous at $x$.
`interior_inter` theorem interior_inter : ∀ {X : Type u} {s t : Set X} [inst : TopologicalSpace X], interior (s ∩ t) = interior s ∩ interior t This theorem states that for any given type `X` in the context of a topological space, and any two sets `s` and `t` of this type, the interior of the intersection of `s` and `t` is equal to the intersection of the interiors of `s` and `t`. In mathematical terms, it expresses that the operation of taking the interior of a set commutes with the operation of taking the intersection of two sets, i.e. $\text{int}(s \cap t) = \text{int}(s) \cap \text{int}(t)$, where "int" denotes the interior of a set in a topological space. More concisely: The interior of the intersection of two sets is equal to the intersection of their interiors in a topological space.
`IsOpen.mem_nhds` theorem IsOpen.mem_nhds : ∀ {X : Type u} {x : X} {s : Set X} [inst : TopologicalSpace X], IsOpen s → x ∈ s → s ∈ nhds x This theorem states that for any type `X` with a topological space structure, any open set `s` of `X`, and any element `x` of `X`, if `x` is an element of `s`, then `s` is a neighborhood of `x`. In other words, if an element `x` belongs to an open set `s`, then `s` is a part of the neighborhood filter at `x`, denoted by `nhds x` in the context of topology. More concisely: For any topological space `(X, τ)` and open set `s ∈ τ` in `X`, if `x ∈ s`, then `s ∈ nhds x`. (In other words, any open set containing an element is a neighborhood of that element.)
`interior_frontier` theorem interior_frontier : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], IsClosed s → interior (frontier s) = ∅ The theorem `interior_frontier` states that for every set `s` of a type `X` embedded in a topological space, if `s` is a closed set, then the interior of the frontier of `s` is the empty set. In other words, the frontier of a closed set in a topological space has no interior points. The frontier of a set is the set of points between the closure and interior of the set. Thus, this theorem essentially states that there are no points that both belong to the frontier of a closed set and are interior points of some open set contained within the frontier. More concisely: The interior of the frontier of any closed subset in a topological space is the empty set.
`Set.Nonempty.of_closure` theorem Set.Nonempty.of_closure : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], (closure s).Nonempty → s.Nonempty This theorem, referred to as `Set.Nonempty.of_closure`, states that for any type `X` with a topology and a set `s` of type `X`, if the closure of `s` is nonempty, then `s` itself is also nonempty. In other words, the theorem ensures that we cannot have a closure of a set being nonempty if the set itself is empty in a topological space. More concisely: If the closure of a set in a topological space is nonempty, then the set itself is nonempty.
`IsClosed.closure_subset_iff` theorem IsClosed.closure_subset_iff : ∀ {X : Type u} {s t : Set X} [inst : TopologicalSpace X], IsClosed t → (closure s ⊆ t ↔ s ⊆ t) This theorem states that for any type `X` with a given topological space structure, and any two sets `s` and `t` of type `X`, if `t` is a closed set, then the closure of `s` is a subset of `t` if and only if `s` itself is a subset of `t`. Here, the closure of a set `s` is defined as the smallest closed set containing `s`. Note that `IsClosed t` checks if `t` is a closed set, and `s ⊆ t` checks if all elements of `s` are also in `t`. More concisely: For any topological space `(X, τ)` and sets `s` and `t` in `X`, `s ⊆ t` implies the closure of `s` is a subset of `t` if and only if `t` is closed.
`isOpen_iff_forall_mem_open` theorem isOpen_iff_forall_mem_open : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], IsOpen s ↔ ∀ x ∈ s, ∃ t ⊆ s, IsOpen t ∧ x ∈ t This theorem, `isOpen_iff_forall_mem_open`, states that for any type `X` and any set `s` of type `X` in the context of a given topological space, the set `s` is open if and only if for every element `x` in `s`, there exists an open set `t` such that `t` is a subset of `s`, and `x` is an element of `t`. In other words, a set is open in a topological space if every point in the set is contained in an open set that is itself contained in the original set. More concisely: A set in a topological space is open if and only if every element in the set is contained in some open subset of the set.
`DenseRange.closure_range` theorem DenseRange.closure_range : ∀ {X : Type u_1} [inst : TopologicalSpace X] {α : Type u_4} {f : α → X}, DenseRange f → closure (Set.range f) = Set.univ This theorem states that for any type `X` equipped with a topological space structure, any type `α`, and any function `f` mapping from `α` to `X`, if `f` has a DenseRange, that is, the image of `f` is a dense subset of `X`, then the closure of the range of `f` equals the universal set of `X`. In simpler terms, if the range of `f` is dense in `X`, it means that every point of `X` is either in the range of `f` or is a limit point of the range, thus taking the closure of the range of `f` (which includes all limit points) results in the entire set `X`. More concisely: If `f` is a continuous function from `α` to a topological space `X` with a dense range, then the closure of `range(f)` equals `X`.
`Filter.Frequently.mem_closure` theorem Filter.Frequently.mem_closure : ∀ {X : Type u} {x : X} {s : Set X} [inst : TopologicalSpace X], (∃ᶠ (x : X) in nhds x, x ∈ s) → x ∈ closure s := by sorry This theorem states that for any type `X` with a topological space structure, any point `x` in `X`, and any set `s` of `X`, if `x` is frequently in `s` in the neighborhood filter of `x`, then `x` is in the closure of `s`. In other words, if there exists a neighborhood of `x` such that `x` is frequently within the set `s`, then `x` is an element of the smallest closed set containing `s`. More concisely: If a point `x` in a topological space `X` belongs to the neighborhood filter of every open set containing a set `s`, then `x` is an element of the closure of `s`.
`preimage_interior_subset_interior_preimage` theorem preimage_interior_subset_interior_preimage : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {t : Set Y}, Continuous f → f ⁻¹' interior t ⊆ interior (f ⁻¹' t) This theorem states that for any two types `X` and `Y`, each equipped with a topological space structure, along with a function `f` from `X` to `Y` and a set `t` of type `Y`, if the function `f` is continuous, then the preimage of the interior of set `t` under `f` is a subset of the interior of the preimage of `t` under `f`. In other words, if you first take the interior of a set and then find the preimage under a continuous function, this will always be a subset of what you get if you first find the preimage of the original set and then take the interior. This theorem is a fundamental property that relates the concepts of continuity, preimages, and interiors in the context of topological spaces. More concisely: For any continuous function between topological spaces and any sets with interiors, the interior of the preimage is contained in the preimage of the interior.
`Function.Surjective.denseRange` theorem Function.Surjective.denseRange : ∀ {X : Type u_1} [inst : TopologicalSpace X] {α : Type u_4} {f : α → X}, Function.Surjective f → DenseRange f := by sorry The theorem `Function.Surjective.denseRange` states that for any topological space `X` and any type `α`, if a function `f` from `α` to `X` is surjective (i.e., for every element of `X` there is some element of `α` such that the function `f` maps that element of `α` to the given element of `X`), then the range of `f` is dense in `X`. In other words, every open subset of `X` contains at least one point from the image of `f`. More concisely: If a function from a type to a topological space is surjective, then its range is dense in the space.
`interior_compl` theorem interior_compl : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], interior sᶜ = (closure s)ᶜ This theorem states that for any set `s` in a given topological space `X`, the interior of the complement of `s` is equal to the complement of the closure of `s`. In other words, it says that taking the interior of the complement of a set is the same as taking the complement of the closure of the original set. This theorem is an important characteristic of the relationship between the interior, closure, and complement operations in topology. More concisely: The interior of a set's complement is equal to the complement of its closure.
`IsClosed.closure_subset` theorem IsClosed.closure_subset : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], IsClosed s → closure s ⊆ s The theorem `IsClosed.closure_subset` states that for any set `s` of type `X` in a topological space, if `s` is a closed set, then the closure of `s` is a subset of `s`. Here, the closure of a set is defined as the smallest closed set containing that set. This theorem essentially tells us that when our original set is already closed, its closure is not any larger than the set itself. More concisely: If `s` is a closed subset of a topological space, then its closure is contained in `s`.
`isOpen_iff_eventually` theorem isOpen_iff_eventually : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], IsOpen s ↔ ∀ x ∈ s, ∀ᶠ (y : X) in nhds x, y ∈ s This theorem states that a set `s` is open if and only if for every point `x` in `s` and every point `y` that is close to `x`, `y` is also in `s`. Here, `X` is a type equipped with a topological space structure and `nhds x` represents the neighborhood filter of `x`. In terms of topology, this theorem captures the intuitive idea of open sets: if a point is in an open set, then all points sufficiently close to it are also in the set. This is essentially a precise formulation of the "without boundary" property of open sets. More concisely: A set in a topological space is open if and only if every point in the set belongs to the neighborhood filter of every point in the set.
`Mathlib.Topology.Basic._auxLemma.7` theorem Mathlib.Topology.Basic._auxLemma.7 : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], IsClosed s = IsOpen sᶜ This theorem states that for any given type `X` and a set `s` of `X` in the context of a topological space, the set `s` is closed if and only if the complement of `s` (`sᶜ`) is open. Here, `IsClosed` denotes that `s` is a closed set in the topological space, and `IsOpen` indicates that a set is open in the topological space. The complement of a set `s`, denoted `sᶜ`, is the set of all elements that are not in `s`. This theorem is a fundamental property of topological spaces in the field of topology. More concisely: A set is closed if and only if its complement is open in a topological space.
`interior_maximal` theorem interior_maximal : ∀ {X : Type u} {s t : Set X} [inst : TopologicalSpace X], t ⊆ s → IsOpen t → t ⊆ interior s The theorem `interior_maximal` states that for any Type `X` and any two sets `s` and `t` of type `X`, given a topology on `X`, if `t` is a subset of `s` and `t` is an open set, then `t` must be a subset of the interior of `s`. In terms of topology, this theorem is saying that the interior of a set is the largest open subset, meaning that any open subset of a set is contained within the interior of that set. More concisely: If `s` is a set in a topological space `X` and `t` is an open subset of `s`, then `t` is a subset of the interior of `s`.
`closure_mono` theorem closure_mono : ∀ {X : Type u} {s t : Set X} [inst : TopologicalSpace X], s ⊆ t → closure s ⊆ closure t := by sorry The theorem `closure_mono` states that for any type `X` with a topological space structure and any two subsets `s` and `t` of `X`, if `s` is a subset of `t`, then the closure of `s` is a subset of the closure of `t`. In other words, the operation of taking closures in a topological space is "monotone": increasing the original set results in an increase of its closure. More concisely: For any topological space (X, τ), and subsets s, t of X with s ⊆ t, the closure of s is contained in the closure of t, denoted ∫s⊆∫t.
`Filter.EventuallyEq.eq_of_nhds` theorem Filter.EventuallyEq.eq_of_nhds : ∀ {X : Type u} {α : Type u_1} {x : X} [inst : TopologicalSpace X] {f g : X → α}, (nhds x).EventuallyEq f g → f x = g x This theorem states that for any type `X` with a topological space structure, any type `α`, and any two functions `f` and `g` from `X` to `α`, if `f` is eventually equal to `g` at the neighborhood filter of a point `x` in `X` (i.e., `f` and `g` are equal at all points sufficiently close to `x`), then the values of `f` and `g` are also equal at `x`. In other words, if two functions coincide in a neighborhood of a point, they must also coincide at that point. More concisely: If two functions from a topological space to a type have equal values in a neighborhood of a point, then they are equal at that point.
`Filter.EventuallyLE.eventuallyLE_nhds` theorem Filter.EventuallyLE.eventuallyLE_nhds : ∀ {X : Type u} {α : Type u_1} {x : X} [inst : TopologicalSpace X] [inst_1 : LE α] {f g : X → α}, (nhds x).EventuallyLE f g → ∀ᶠ (y : X) in nhds x, (nhds y).EventuallyLE f g This theorem states that, given a topological space `X` and two functions `f` and `g` from `X` to a type `α` equipped with a less-than-or-equal-to relation, if `f x ≤ g x` is true in a neighborhood around a point `x`, then for any point `y` sufficiently close to `x` (i.e., in the neighborhood of `x`), `f x ≤ g x` is also true in a neighborhood around `y`. More concisely: Given a topological space `X` and functions `f` and `g` from `X` to a type `α` with a total order, if `f(x) ≤ g(x)` holds in a neighborhood of `x`, then it holds in a neighborhood of any point `y` sufficiently close to `x`.
`exists_open_set_nhds` theorem exists_open_set_nhds : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X] {U : Set X}, (∀ x ∈ s, U ∈ nhds x) → ∃ V, s ⊆ V ∧ IsOpen V ∧ V ⊆ U The theorem `exists_open_set_nhds` states that in any topological space `X`, if a set `U` is a neighborhood of each point `x` in another set `s`, then `U` is also a neighborhood of the set `s` as a whole. In other words, `U` contains an open set `V` that contains `s`. Specifically, for every point `x` in `s`, `U` is in the neighborhood filter of `x`. This then implies the existence of an open set `V` such that `s` is a subset of `V`, `V` is an open set, and `V` is a subset of `U`. More concisely: If a set U is a neighborhood of every point in another set s in a topological space, then there exists an open set V containing s that is a subset of U.
`Dense.inter_open_nonempty` theorem Dense.inter_open_nonempty : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], Dense s → ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty The theorem `Dense.inter_open_nonempty` states that for any type `X` and set `s` within a topological space, if `s` is dense, then for any set `U` that is open and nonempty, the intersection of `U` and `s` is also nonempty. In other words, a set is dense in a topological space if it intersects every nonempty open set in a nonempty way. More concisely: If `s` is a dense subset of a topological space `X`, then for any open and nonempty set `U` in `X`, the intersection `U ∩ s` is nonempty.
`Mathlib.Topology.Basic._auxLemma.4` theorem Mathlib.Topology.Basic._auxLemma.4 : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], IsOpen sᶜ = IsClosed s This theorem states that for any type `X` and a set `s` of this type, given that `X` has a topological space structure, the complement of `s` is open if and only if `s` is closed in this topological space. In mathematical terms, given a set `s` in a topological space `X`, the complement of `s` (denoted as `sᶜ`) is an open set if and only if the set `s` is a closed set in the topological space `X`. More concisely: In a topological space, a set and its complement are open if and only if each other is closed.
`subset_closure` theorem subset_closure : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], s ⊆ closure s This theorem states that for any type `X` and any set `s` of type `X` in a given topological space, `s` is a subset of its closure. In other words, for all sets in a topological space, every element of the set is also an element of the set's closure. This is a fundamental property of closures in topology. More concisely: For any topological space and set `s` of type `X`, every element of `s` belongs to the closure of `s`.
`Set.Nonempty.closure` theorem Set.Nonempty.closure : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], s.Nonempty → (closure s).Nonempty This theorem, also known as an alias of the reverse direction of `closure_nonempty_iff`, expresses that for any type `X` and a set `s` of `X` operating under a specified topological space, if the set `s` is non-empty, then the closure of the set `s` is also non-empty. In other words, it asserts that the closure operation preserves the non-emptiness property of a set in topological spaces. More concisely: If a non-empty set `s` in a topological space has a closure, then the closure of `s` is non-empty.
`continuous_iff_continuousAt` theorem continuous_iff_continuousAt : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}, Continuous f ↔ ∀ (x : X), ContinuousAt f x This theorem is stating that for any two types `X` and `Y` that have topological space structures, a function `f` between `X` and `Y` is continuous if and only if it is continuous at every point in `X`. In mathematical terms, a function `f` mapping `X` to `Y` is continuous if the preimage of every open set in `Y` is open in `X`. This is equivalent to saying that for any point `x` in `X`, the function `f` is continuous at `x`, meaning the function `f` applied to any sequence in `X` that converges to `x` also converges to `f(x)` in `Y`. More concisely: A function between two topological spaces is continuous if and only if it maps every open set to an open set.
`IsOpen.eventually_mem` theorem IsOpen.eventually_mem : ∀ {X : Type u} {x : X} {s : Set X} [inst : TopologicalSpace X], IsOpen s → x ∈ s → ∀ᶠ (x : X) in nhds x, x ∈ s := by sorry This theorem, `IsOpen.eventually_mem`, states that for any topological space `X`, any point `x` in `X`, and any set `s` of `X`, if `s` is an open set and `x` is an element of `s`, then eventually, all points in the neighborhood (defined by the neighborhood filter `nhds`) of `x` will also be elements of `s`. In other words, if `x` is in an open set `s`, then points sufficiently close to `x` are also in `s`, which aligns with the intuitive sense of open sets in topology. More concisely: For any topological space X, point x in X, and open set s in X containing x, there exists a neighborhood N of x such that N ⊆ s.
`isOpen_compl_iff` theorem isOpen_compl_iff : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], IsOpen sᶜ ↔ IsClosed s This theorem, `isOpen_compl_iff`, establishes a relationship between open and closed sets in a given topological space `X`. Specifically, it states that for any set `s` of type `X`, the set `s` is closed if and only if the complement of `s` (denoted as `sᶜ`) is open in the topology of `X`. This is a fundamental property in topology connecting the concepts of open and closed sets. More concisely: A set in a topological space is closed if and only if its complement is open.
`interior_eq_iff_isOpen` theorem interior_eq_iff_isOpen : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], interior s = s ↔ IsOpen s := by sorry This theorem, `interior_eq_iff_isOpen`, states that for any type `X` and any set `s` of type `X`, given the context of a topological space, the interior of the set `s` is equal to `s` if and only if `s` is an open set. In other words, in the context of a topological space, a set is open if and only if it is equal to its own interior. This theorem provides a way to check if a set is open by comparing it with its interior. More concisely: In a topological space, a set is open if and only if it equals its interior.
`Continuous.comp` theorem Continuous.comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z] {f : X → Y} {g : Y → Z}, Continuous g → Continuous f → Continuous (g ∘ f) This theorem states that for any three types `X`, `Y`, and `Z`, where each type is equipped with a topological space structure, if `f` is a continuous function from `X` to `Y` and `g` is a continuous function from `Y` to `Z`, then the composition of `g` and `f` (denoted by `g ∘ f`) is also a continuous function. This is a fundamental theorem in topology known as the composition of continuous functions theorem. More concisely: If `f` is a continuous function from type `X` to `Y` and `g` is a continuous function from type `Y` to `Z`, then the composition `g ∘ f` is a continuous function from `X` to `Z`.
`eventually_eventually_nhds` theorem eventually_eventually_nhds : ∀ {X : Type u} {x : X} [inst : TopologicalSpace X] {p : X → Prop}, (∀ᶠ (y : X) in nhds x, ∀ᶠ (x : X) in nhds y, p x) ↔ ∀ᶠ (x : X) in nhds x, p x This theorem states that for any topological space `X` and any point `x` in `X`, a property `p` holds eventually for all points in a neighborhood of `x`, if and only if `p` holds eventually for all points in a neighborhood of every point in the neighborhood of `x`. Here, "eventually" refers to the mathematical concept implying that beyond a certain point in a sequence or function, all subsequent terms or values satisfy a given property. Also, "neighborhood" is used in the topological sense where it refers to a set that includes an open set containing the point. More concisely: For any topological space X and point x, a property p holds eventually for all points in a neighborhood of x if and only if it holds eventually for all points in the neighborhood of any point in that neighborhood.
`Filter.Eventually.self_of_nhds` theorem Filter.Eventually.self_of_nhds : ∀ {X : Type u} {x : X} [inst : TopologicalSpace X] {p : X → Prop}, (∀ᶠ (y : X) in nhds x, p y) → p x The theorem `Filter.Eventually.self_of_nhds` asserts that if a property or predicate `p` holds true in a neighborhood of a point `x` in a topological space `X`, then that property `p` is also true for the point `x` itself. In more mathematical terminology, this theorem states that if for every neighborhood of `x` (in the sense of the neighborhood filter `nhds x`), there exists a point `y` where the predicate `p` holds, then `p` must also hold for `x`. More concisely: If every neighborhood of a point `x` in a topological space `X` contains a point `y` where property `p` holds, then `p` holds for `x` itself.
`closure_compl_singleton` theorem closure_compl_singleton : ∀ {X : Type u} [inst : TopologicalSpace X] (x : X) [inst_1 : (nhdsWithin x {x}ᶜ).NeBot], closure {x}ᶜ = Set.univ This theorem states that in any topological space, if a point 'x' is not isolated, meaning it has neighborhood not exclusively consisting of itself, then the closure of the complement of the singleton set containing 'x' is the entire space. Here, the closure of a set is the smallest closed set containing the set, and the complement of a set contains all points not in the set. Thus, this theorem is stating that all points of the topological space are either in the complement of the singleton set or can be approximated by a sequence of points from this complement, if 'x' is not an isolated point. More concisely: In a topological space, if a point is not isolated, then its closure equals the entire space, and every point is in the closure of the complement of that point.
`mem_closure_iff_frequently` theorem mem_closure_iff_frequently : ∀ {X : Type u} {x : X} {s : Set X} [inst : TopologicalSpace X], x ∈ closure s ↔ ∃ᶠ (x : X) in nhds x, x ∈ s := by sorry The theorem `mem_closure_iff_frequently` states that for any type `X`, any element `x` of `X`, and any set `s` of `X`, under a given topological space, `x` belongs to the closure of `s` if and only if, frequently in the neighbourhood filter at `x`, `x` belongs to `s`. In other words, an element is in the closure of a set if it is frequently in that set when considering neighborhoods around it. More concisely: An element belongs to the closure of a set in a topological space if and only if it is in the set frequently in the neighborhood filter at that element.
`dense_compl_singleton_iff_not_open` theorem dense_compl_singleton_iff_not_open : ∀ {X : Type u} {x : X} [inst : TopologicalSpace X], Dense {x}ᶜ ↔ ¬IsOpen {x} This theorem states that for any type `X` and any element `x` of type `X`, with a given topological space structure on `X`, the complement of the set containing only `x` is dense if and only if the set containing only `x` is not open. In the context of topology, a set is dense if any point of the topological space belongs to its closure, and a set is open if it belongs to the given topology. Thus, essentially, the theorem is saying that in a certain topological space, complete coverage of the space (aside from a single point `x`) is equivalent to the assertion that the set containing only `x` is not an open set. More concisely: In a topological space, a singleton set is dense if and only if it is not open.
`mem_closure_iff_clusterPt` theorem mem_closure_iff_clusterPt : ∀ {X : Type u} {x : X} {s : Set X} [inst : TopologicalSpace X], x ∈ closure s ↔ ClusterPt x (Filter.principal s) This theorem states that for any type `X`, for any point `x` in `X`, and for any set `s` of `X`, given that `X` has a topology, `x` is in the closure of `s` if and only if `x` is a cluster point of the principal filter of `s`. In other words, a point is in the smallest closed set containing a particular set precisely when it is a cluster point, i.e., the point where every open set containing it intersects with the given set, of the collection of all supersets of the given set. More concisely: A point in a topological space is in the closure of a set if and only if it is a cluster point of the principal filter generated by the set.
`IsOpen.isClosed_compl` theorem IsOpen.isClosed_compl : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsOpen s → IsClosed sᶜ := by sorry This theorem, denoted as `IsOpen.isClosed_compl`, states that for any type `X` equipped with a topological space structure, and for any set `s` of this type `X`, if the set `s` is open in this topological space, then the complement of `s`, denoted as `sᶜ`, is a closed set in the same topological space. In mathematical terms, this theorem captures one of the fundamental concepts of topology, which is that the complement of an open set is always a closed set. More concisely: If a set is open in a topological space, then its complement is closed.
`continuousAt_id` theorem continuousAt_id : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X}, ContinuousAt id x This theorem states that the identity function is continuous at every point in any topological space. In mathematical terms, for any topological space `X` and any point `x` in `X`, the identity function `id` satisfies the property that `id(x)` tends to `id(x₀)` when `x` tends to `x₀`. Here, `id(x)` is simply `x`, so the property simplifies to `x` tends to `x₀` when `x` tends to `x₀`, which is always true. More concisely: The identity function is continuous on every topological space.
`isOpen_singleton_iff_nhds_eq_pure` theorem isOpen_singleton_iff_nhds_eq_pure : ∀ {X : Type u} [inst : TopologicalSpace X] (x : X), IsOpen {x} ↔ nhds x = pure x This theorem states that for any type `X` equipped with a topology and any element `x` of `X`, the singleton set containing just `x` is an open set if and only if the neighborhood filter at `x` is equal to the pure filter at `x`. In other words, a single-element set is open in the given topological space if and only if every neighborhood of the element contains only that element. More concisely: A singleton set in a topological space is open if and only if it is the only element in every neighborhood of its element.
`Filter.EventuallyEq.tendsto` theorem Filter.EventuallyEq.tendsto : ∀ {X : Type u} {α : Type u_1} {x : X} [inst : TopologicalSpace X] {l : Filter α} {f : α → X}, (l.EventuallyEq f fun x_1 => x) → Filter.Tendsto f l (nhds x) The theorem `Filter.EventuallyEq.tendsto` states that for any types `X` and `α`, any point `x` of type `X`, any topological space over `X`, any filter `l` of type `α`, and any function `f` from `α` to `X`, if `f` is eventually equal (almost everywhere) to the constant function that always returns `x` (denoted as `(f =ᶠ[l] fun x_1 => x)`), then `f` tends to `x` with respect to the filter `l` (denoted as `Filter.Tendsto f l (nhds x)`). In other words, if a function equals a constant almost everywhere with respect to some filter, then the function tends to that constant in the topological space's neighborhood filter. This is a specific instance of the concept of limit in topology. More concisely: If a function is almost equal to a constant function with respect to a filter in a topological space, then the function converges to the constant value in the filter's neighborhood filter.
`nhds_basis_opens` theorem nhds_basis_opens : ∀ {X : Type u} [inst : TopologicalSpace X] (x : X), (nhds x).HasBasis (fun s => x ∈ s ∧ IsOpen s) fun s => s := by sorry The theorem `nhds_basis_opens` states that for any topological space `X` and any point `x` in `X`, the open sets containing `x` form a basis for the neighborhood filter of `x`. In other words, the neighborhood filter of `x` can be generated from the collection of all open sets that contain `x`. This theorem provides a fundamental characterization of the structure of the neighborhood filter in terms of open sets, which is a key concept in topology. More concisely: The neighborhood filter of a point in a topological space can be generated by the collection of open sets containing that point.
`closure_closure` theorem closure_closure : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], closure (closure s) = closure s := by sorry The theorem `closure_closure` states that for any type `X` and any set `s` of type `X`, given that `X` has a topological space structure, the closure of the closure of `s` is equal to the closure of `s`. In other words, taking successive closures of a set does not change the set after the first closure. This is important in topology because the closure of a set, which includes the set itself along with its limit points, provides a way to 'complete' the set in the surrounding space. More concisely: For any topological space (X, τ) and subset s ∈ X, the closure of the closure of s equals the closure of s. In symbols, cl(cl(s)) = cl(s).
`Filter.le_lift'_closure` theorem Filter.le_lift'_closure : ∀ {X : Type u} [inst : TopologicalSpace X] (l : Filter X), l ≤ l.lift' closure := by sorry This theorem states that for any type `X` equipped with a topological space structure and any filter `l` on `X`, the filter `l` is less than or equal to the filter obtained by applying the `lift'` operation to `l` with the `closure` operation. In other words, every element of `l` is also an element of the filter generated by taking the closure of each set in `l`. This means that the filter `l` is contained within the filter of all closure sets of `l`. More concisely: For any topological space `(X, τ)` and filter `l` on `X`, `l ⊆ closure (l'_ filter τ l)`. (Here, `l'_ filter` denotes the filter obtained by applying `lift` to `l` in Lean.)
`interior_mem_nhds` theorem interior_mem_nhds : ∀ {X : Type u} {x : X} {s : Set X} [inst : TopologicalSpace X], interior s ∈ nhds x ↔ s ∈ nhds x This theorem states that for any type `X`, any element `x` of `X`, and any set `s` of `X`, given a topology on `X`, the interior of `s` is in the neighborhood of `x` if and only if `s` itself is in the neighborhood of `x`. In other words, it establishes a connection between a particular set `s` and its interior in terms of their relationship to the neighborhood of a given point `x` in the context of a topological space. More concisely: For any topological space (X, τ), point x ∈ X, and set s ∈ τ, the interior of s contains x if and only if s is in the neighborhood of x.
`Set.MapsTo.closure_left` theorem Set.MapsTo.closure_left : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X} {t : Set Y}, Set.MapsTo f s t → Continuous f → IsClosed t → Set.MapsTo f (closure s) t The theorem `Set.MapsTo.closure_left` states that given two types `X` and `Y`, each equipped with a topology, and a continuous map `f` from `X` to `Y`, if the image of a set `s` in `X` under `f` is contained within a closed set `t` in `Y`, then the image of the closure of `s` (which is the smallest closed set containing `s`) under `f` is also contained within `t`. In other words, a continuous map from `X` to `Y` that maps `s` into `t` will also map the closure of `s` into `t`, provided that `t` is a closed set in `Y`. More concisely: If `f` is a continuous map from a topological space `(X, τx)` to another topological space `(Y, τy)`, `s ⊆ X` is a set, `t ⊆ Y` is closed, and `f(s) ⊆ t`, then `f(cl(s)) ⊆ t`, where `cl(s)` denotes the closure of `s` in `X`.
`Continuous.continuousAt` theorem Continuous.continuousAt : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {x : X}, Continuous f → ContinuousAt f x This theorem states that for any two types `X` and `Y` equipped with a topological structure (i.e., they are topological spaces), and any function `f` from `X` to `Y`, if the function `f` is continuous, then it is also continuous at any point `x` in `X`. In mathematical terms, if `f` is a continuous function, then for every point `x` in the domain, the function values `f(x)` approach `f(x₀)` as `x` approaches `x₀`. More concisely: If `f` is a continuous function between topological spaces `X` and `Y`, then `f` is continuous at every point `x` in `X`.
`Mathlib.Topology.Basic._auxLemma.20` theorem Mathlib.Topology.Basic._auxLemma.20 : ∀ {α : Type u} {s : Set α}, s.Nonempty = (s ≠ ∅) This theorem states that for any type `α` and any set `s` of type `α`, the property that `s` is nonempty (i.e., `Set.Nonempty s`) is equivalent to the statement that `s` is not the empty set (i.e., `s ≠ ∅`). This establishes an equivalence between two different ways of expressing the non-emptiness of a set. More concisely: The theorem asserts that a set `s` of type `α` is nonempty if and only if it is not equal to the empty set. In Lean notation, `Set.Nonempty s ��nvdash= s ≠ ∅`.
`interior_interior` theorem interior_interior : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], interior (interior s) = interior s The theorem `interior_interior` states that for any type `X` and for any set `s` of type `X` under a certain topological space `inst`, the interior of the interior of `s` is equal to the interior of `s`. In other words, in the context of topology, taking the interior of a set twice does not change the set, i.e., the operation of finding the interior of a set is idempotent. More concisely: For any topological space `(X, inst)` and set `s : X`, the interior of the interior of `s` equals the interior of `s`: `interior (interior s) = interior s`.
`AccPt.mono` theorem AccPt.mono : ∀ {X : Type u} {x : X} [inst : TopologicalSpace X] {F G : Filter X}, AccPt x F → F ≤ G → AccPt x G This theorem states that if `x` is an accumulation point of a filter `F` in a topological space `X`, and `F` is a subset of another filter `G` (in the sense that `F ≤ G`), then `x` is also an accumulation point of `G`. An accumulation point of a filter, roughly speaking, is a point in the topological space where the filter "accumulates". In other words, any open set containing the point will intersect with the set of filter elements. More concisely: If `F ≤ G` are filters in a topological space `X` and `x` is an accumulation point of `F`, then `x` is an accumulation point of `G`.
`Dense.exists_mem_open` theorem Dense.exists_mem_open : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], Dense s → ∀ {U : Set X}, IsOpen U → U.Nonempty → ∃ x ∈ s, x ∈ U The theorem `Dense.exists_mem_open` states that for any topological space `X` and any set `s` in this space, if `s` is dense in `X`, then for any set `U` in `X` that is open and nonempty, there exists an element `x` that belongs to both `s` and `U`. In other words, in any nonempty open set in the topological space, we can always find a point from the dense set. This is a fundamental property of dense sets in topology. More concisely: If a dense subset of a topological space is non-empty, then for any open set in the space, there exists an element in the dense subset that belongs to the open set.
`Dense.closure` theorem Dense.closure : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], Dense s → Dense (closure s) This theorem, referred to as an alias of the reverse direction of `dense_closure`, states that for any topological space `X` and any set `s` in `X`, if `s` is dense in `X`, then the closure of `s` (which is the smallest closed set containing `s`) is also dense in `X`. In mathematical terms, `s` being dense means that every point in `X` is either in `s` or is a limit point of `s` (belongs to the closure of `s`). The theorem essentially asserts that the property of denseness is preserved under taking the closure of a set in a topological space. More concisely: If a set is dense in a topological space, then its closure is also dense in that space.
`Mathlib.Topology.Basic._auxLemma.75` theorem Mathlib.Topology.Basic._auxLemma.75 : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], IsClosed s = ∀ (a : X), ClusterPt a (Filter.principal s) → a ∈ s This theorem states that, for any type `X` and a set `s` of type `X` in a topological space, the set `s` is closed if and only if for every element `a` of type `X`, if `a` is a cluster point of the principal filter of `s`, then `a` belongs to `s`. In more mathematical terms, a set `s` in a topological space is closed if for every point `a`, if every neighborhood of `a` intersects with `s` (meaning `a` is a cluster point of `s`), then `a` is an element of `s`. This is essentially the definition of a closed set - a set which contains all its limit points or cluster points. More concisely: A set in a topological space is closed if and only if it contains all its cluster points.
`Filter.Eventually.eventually_nhds` theorem Filter.Eventually.eventually_nhds : ∀ {X : Type u} {x : X} [inst : TopologicalSpace X] {p : X → Prop}, (∀ᶠ (y : X) in nhds x, p y) → ∀ᶠ (y : X) in nhds x, ∀ᶠ (x : X) in nhds y, p x The theorem `Filter.Eventually.eventually_nhds` states that in a topological space, if a certain property or condition holds true in a neighborhood of a point `x`, then for all points `y` that are sufficiently close to `x`, this property will also hold true in a neighborhood of `y`. In other words, if a property is locally true at a point, then it's also true at points close to it. More concisely: If a property holds in the neighborhood of a point in a topological space, then it holds in the neighborhood of any point sufficiently close to it.
`IsOpen.mem_nhds_iff` theorem IsOpen.mem_nhds_iff : ∀ {X : Type u} {x : X} {s : Set X} [inst : TopologicalSpace X], IsOpen s → (s ∈ nhds x ↔ x ∈ s) This theorem states that for any type `X`, any element `x` of type `X`, and any set `s` of elements of type `X`, given a topological structure on `X`, if `s` is an open set, then `s` is a neighborhood of `x` (i.e., `s` belongs to the neighborhood filter of `x`) if and only if `x` belongs to `s`. In mathematical terms, for an open set `s` in a topological space, `s` is a neighborhood of an element `x` if and only if `x` is an element of `s`. More concisely: In a topological space, an open set is a neighborhood of an element if and only if that element is a member of the set.
`Mathlib.Topology.Basic._auxLemma.52` theorem Mathlib.Topology.Basic._auxLemma.52 : ∀ {a b : Prop}, (a ∧ b) = (b ∧ a) This theorem, named `Mathlib.Topology.Basic._auxLemma.52`, states the commutative property of logical conjunction. Given any two propositional variables `a` and `b`, the proposition "`a` and `b`" is equivalent to the proposition "`b` and `a`". That is, the conjunction of `a` and `b` is the same as the conjunction of `b` and `a`. In other words, the order in which the propositions are conjoined does not change the truth value of the statement. More concisely: The theorem `Mathlib.Topology.Basic._auxLemma.52` asserts the commutativity of logical conjunction, that is, `a ∧ b ≡ b ∧ a` for all propositional variables `a` and `b`.
`monotone_closure` theorem monotone_closure : ∀ (X : Type u_3) [inst : TopologicalSpace X], Monotone closure The theorem `monotone_closure` states that for any type `X` equipped with a topology (i.e., `X` is a topological space), the function `closure` is monotone. In other words, for any two sets `a` and `b` in `X`, if `a` is a subset of `b`, then the closure of `a` is also a subset of the closure of `b`. This essentially means that taking the closure of a set preserves the subset relationship. More concisely: The closure operation on a topological space is monotone, that is, for any sets `a` and `b` such that `a` is a subset of `b`, we have `closure(a)` is a subset of `closure(b)`.
`isClosed_empty` theorem isClosed_empty : ∀ {X : Type u} [inst : TopologicalSpace X], IsClosed ∅ This theorem states that for any type `X` equipped with a topology (i.e., `X` is a topological space), the empty set is a closed set. In mathematical terms, this is the assertion that in any topological space, the empty set is always considered closed, which is a fundamental property in topology. More concisely: In any topological space, the empty set is a closed set.
`closure_diff_interior` theorem closure_diff_interior : ∀ {X : Type u} [inst : TopologicalSpace X] (s : Set X), closure s \ interior s = frontier s The theorem `closure_diff_interior` states that for any set `s` in a given topological space `X`, the difference between the closure of `s` and the interior of `s` is equal to the frontier of `s`. In other words, the set of all points that are either in the closure of `s` but not in its interior defines the frontier of `s`. Here, the closure of a set is the smallest closed set containing it, the interior of a set is its largest open subset, and the frontier of a set includes all points between its closure and interior. More concisely: The closure of a set in a topological space equals the union of its interior and frontier, and the difference between the two is the frontier.
`eventuallyEq_zero_nhds` theorem eventuallyEq_zero_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X} {M₀ : Type u_4} [inst_1 : Zero M₀] {f : X → M₀}, (nhds x).EventuallyEq f 0 ↔ x ∉ closure (Function.support f) This theorem, which is deprecated in favor of `not_mem_tsupport_iff_eventuallyEq`, relates the neighborhood filter of a point in a topological space to the closure set and function support. Specifically, it states that for any topological space 'X', any point 'x' in 'X', any type 'M₀' with zero element, and any function 'f' mapping 'X' to 'M₀', the condition that the function 'f' is eventually equal to zero at the neighborhood of 'x' is equivalent to 'x' not being a part of the closure of the support of 'f'. The support of 'f' is the set of points where 'f' does not equal zero. The closure of a set is the smallest closed set that contains the given set. More concisely: The theorem states that in a topological space, a point is not in the closure of a function's support if and only if the function is eventually equal to zero in the neighborhood of that point.
`Mathlib.Topology.Basic._auxLemma.5` theorem Mathlib.Topology.Basic._auxLemma.5 : ∀ {X : Type u} [inst : TopologicalSpace X], IsClosed ∅ = True This theorem states that for any type `X`, endowed with a `TopologicalSpace` structure, the empty set is always a closed set. In other words, in the context of a given topological space, the empty set is always considered closed regardless of the specific type of `X` or the specifics of the topology. More concisely: In any topological space, the empty set is a closed set.
`IsClosed.frontier_eq` theorem IsClosed.frontier_eq : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], IsClosed s → frontier s = s \ interior s The theorem `IsClosed.frontier_eq` states that for any type `X` with a `TopologicalSpace` instance, and for any set `s` of type `X`, if `s` is a closed set, then the frontier of `s` is equal to the set difference of `s` and the interior of `s`. Here, the frontier of a set is defined as the set of points between the closure and the interior of the set, and the interior of a set `s` is the largest open subset of `s`. More concisely: For any topological space `X` and closed set `s` in `X`, the frontier of `s` is equal to the set difference between `s` and its interior.
`tendsto_const_nhds` theorem tendsto_const_nhds : ∀ {X : Type u} {α : Type u_1} {x : X} [inst : TopologicalSpace X] {f : Filter α}, Filter.Tendsto (fun x_1 => x) f (nhds x) The theorem `tendsto_const_nhds` states that for any topological space `X`, any filter `f` on a type `α`, and any element `x` of `X`, the constant function that sends any element to `x` is continuous at `x` with respect to the filter `f` and the neighborhood filter at `x`. In other words, for every neighborhood of `x`, the preimage of this neighborhood under the constant function is in the filter `f`, thus indicating that the function "converges" to `x` according to the filter `f`. More concisely: For any topological space X, filter f on α, and x ∈ X, the constant function from α to x is continuous at x with respect to filter f iff for every neighborhood V of x in X, the preimage x⁁⁻¹(V) is in the filter f.
`isClosed_closure` theorem isClosed_closure : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], IsClosed (closure s) This theorem states that for any type `X` and for any set `s` of type `X`, given that `X` has a topology, the closure of `s` is a closed set. In mathematical terms, `closure s` represents the smallest closed set that contains all elements of `s` in a topological space. The theorem ensures that the result of this closure operation is indeed a closed set in the given topological space. More concisely: In a topological space, the closure of any set is a closed set.
`interior_eq_empty_iff_dense_compl` theorem interior_eq_empty_iff_dense_compl : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], interior s = ∅ ↔ Dense sᶜ The theorem `interior_eq_empty_iff_dense_compl` states that for any type `X` and a set `s` of `X` in a given topological space, the interior of `s` is empty if and only if the complement of `s` (`sᶜ`) is dense in that topological space. In other words, it says that a set's interior being empty is equivalent to every point in the topological space belonging to the closure of the set's complement. More concisely: A set's interior is empty if and only if its complement is dense in the topological space.
`image_closure_subset_closure_image` theorem image_closure_subset_closure_image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X}, Continuous f → f '' closure s ⊆ closure (f '' s) This theorem states that for any two types `X` and `Y` with given topological structures, a function `f` from `X` to `Y`, and a set `s` of type `X`, if the function `f` is continuous, then the image of the closure of set `s` under function `f` is a subset of the closure of the image of set `s` under function `f`. In mathematical terms, if `f` is a continuous map, `f(closure(s)) ⊆ closure(f(s))` where `closure` represents the operation of taking the topological closure of a set. More concisely: For any continuous function `f` between topological spaces `X` and `Y`, and any set `s` in `X`, the image of the closure of `s` under `f` is contained in the closure of the image of `s` under `f`: `f(closure(s)) ⊆ closure(f(s))`.
`mem_closure_iff` theorem mem_closure_iff : ∀ {X : Type u} {x : X} {s : Set X} [inst : TopologicalSpace X], x ∈ closure s ↔ ∀ (o : Set X), IsOpen o → x ∈ o → (o ∩ s).Nonempty The theorem `mem_closure_iff` states that for any type `X`, any element `x` of `X`, and any set `s` of `X` in a given topological space, `x` is an element of the closure of `s` if and only if for every open set `o` containing `x`, the intersection of `o` and `s` is nonempty. This essentially means that `x` is in the closure of `s` whenever it is contained in an open set that intersects `s`. More concisely: For any topological space, an element is in the closure of a set if and only if there exists an open set containing the element that intersects the set non-empty.
`ClusterPt.of_le_nhds'` theorem ClusterPt.of_le_nhds' : ∀ {X : Type u} {x : X} [inst : TopologicalSpace X] {f : Filter X}, f ≤ nhds x → f.NeBot → ClusterPt x f The theorem `ClusterPt.of_le_nhds'` states that for any type `X` equipped with a topology, any point `x` in `X`, and any filter `f` on `X`, if `f` is greater than or equal to the neighborhood filter at `x` and `f` is not the bottom filter, then `x` is a cluster point of the filter `f`. In other words, it asserts that if a filter `f` doesn't contain the empty set and includes all neighborhood sets of `x`, then `x` is a limit point of `f`, meaning that every neighborhood of `x` contains a point in `f`. More concisely: If a filter on a topological space contains the neighborhood filter of a point and is not the bottom filter, then that point is a cluster point of the filter.
`IsOpen.sdiff` theorem IsOpen.sdiff : ∀ {X : Type u} {s t : Set X} [inst : TopologicalSpace X], IsOpen s → IsClosed t → IsOpen (s \ t) The theorem `IsOpen.sdiff` states that for any type `X` and any two sets `s` and `t` of type `X` in a given topological space, if `s` is an open set and `t` is a closed set, then the set difference `s \ t` is an open set. In other words, the result of subtracting a closed set from an open set in a topological space is always an open set. More concisely: If `s` is an open set and `t` is a closed set in a topological space, then their set difference `s \ t` is an open set.
`ContinuousAt.congr` theorem ContinuousAt.congr : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {x : X} {g : X → Y}, ContinuousAt f x → (nhds x).EventuallyEq f g → ContinuousAt g x The theorem `ContinuousAt.congr` states that for any two functions `f` and `g` from a topological space `X` to a topological space `Y`, and any point `x` in `X`, if `f` is continuous at `x` and `g` is equal to `f` in a neighborhood of `x` (represented by the filter `nhds x`), then `g` is also continuous at `x`. Essentially, it says that if two functions coincide in a neighborhood of a point, and one of them is continuous at that point, then the other is too. More concisely: If a function `f` is continuous at a point `x` in a topological space `X` and `f` equals `g` in a neighborhood of `x`, then `g` is also continuous at `x` in `X` to `Y`.
`isClosed_of_closure_subset` theorem isClosed_of_closure_subset : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], closure s ⊆ s → IsClosed s The theorem `isClosed_of_closure_subset` states that for any type `X` and any set `s` of `X`, given a topology on `X`, if the closure of `s` is a subset of `s`, then `s` is a closed set. The closure of a set `s` is the smallest closed set that contains `s`. So, if this closure still fits within `s` itself, it implies that `s` is closed in the given topological space. More concisely: If the closure of a set is a subset of the set in a topology, then the set is closed.
`closure_eq_iff_isClosed` theorem closure_eq_iff_isClosed : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], closure s = s ↔ IsClosed s This theorem states that for any set `s` of a certain type `X` in a topological space, the closure of `s` is equal to `s` if and only if `s` is a closed set. In other words, a set is equal to its own closure (the smallest closed set that contains it) if and only if it is a closed set within the context of the given topological space. More concisely: A set in a topological space is closed if and only if it is equal to its closure.
`isClosed_frontier` theorem isClosed_frontier : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], IsClosed (frontier s) This theorem states that the frontier of a set is always a closed set. More specifically, for any type `X` and any set `s` of type `X`, given that `X` has a topological space structure, the frontier of `s` (which is the set of points that lie between the closure and the interior of `s`) is a closed set in the topological space of `X`. More concisely: The frontier of a set in a topological space is a closed set.
`continuousAt_const` theorem continuousAt_const : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x : X} {y : Y}, ContinuousAt (fun x => y) x This theorem, named `continuousAt_const`, states that for any two types `X` and `Y` both equipped with a topological space structure, a function that maps any element `x` from `X` to a fixed element `y` from `Y` is continuous at `x`. In mathematical terms, it asserts that a constant function is always continuous at any point in its domain. More concisely: For any topological spaces X and Y and any fixed y : Y, the constant function from X to y is continuous.
`IsOpen.union` theorem IsOpen.union : ∀ {X : Type u} {s₁ s₂ : Set X} [inst : TopologicalSpace X], IsOpen s₁ → IsOpen s₂ → IsOpen (s₁ ∪ s₂) The theorem `IsOpen.union` states that for any type `X` that has a topological space structure, if `s₁` and `s₂` are sets of elements of type `X` and both `s₁` and `s₂` are open in this topological space, then their union `s₁ ∪ s₂` is also open in this topological space. This is a basic property in topology that the union of two open sets is itself an open set. More concisely: If `X` is a topological space and `s₁` and `s₂` are open sets in `X`, then their union `s₁ ∪ s₂` is also an open set in `X`.
`dense_closure` theorem dense_closure : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], Dense (closure s) ↔ Dense s This theorem states that for any type `X` and a set `s` of type `X` within a topological space, the closure of `s` is dense if and only if `s` itself is dense. In the context of topology, a set is dense if every point in the space belongs to the closure of the set. Here, the closure of a set is defined as the smallest closed set that contains the set. Therefore, this theorem is asserting an equivalence between the density of a set and the density of its closure in a given topological space. More concisely: A set and its closure have the same density in a topological space.
`isClosed_iff_clusterPt` theorem isClosed_iff_clusterPt : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], IsClosed s ↔ ∀ (a : X), ClusterPt a (Filter.principal s) → a ∈ s This theorem states that for any type `X` and a set `s` of `X` under a certain topological space, the set `s` is closed if and only if for every point `a` in `X`, if `a` is a cluster point of the principal filter of `s`, then `a` belongs to `s`. In other words, a set is closed when all of its cluster points, with respect to the principal filter of the set, are contained within the set itself. More concisely: A set `s` under a topological space is closed if and only if every cluster point of `s` with respect to its principal filter belongs to `s`.
`dense_iff_closure_eq` theorem dense_iff_closure_eq : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], Dense s ↔ closure s = Set.univ This theorem states that for any set `s` in a topological space `X`, `s` is dense if and only if the closure of `s` equals the universal set. In other words, a set is considered dense in a topological space if every point in the space is either in the set or is a limit point of the set, which corresponds to the closure of the set being the entire space. More concisely: A set is dense in a topological space if and only if its closure equals the entire space.
`Set.Finite.isOpen_biInter` theorem Set.Finite.isOpen_biInter : ∀ {X : Type u} {α : Type u_1} [inst : TopologicalSpace X] {s : Set α} {f : α → Set X}, s.Finite → (∀ i ∈ s, IsOpen (f i)) → IsOpen (⋂ i ∈ s, f i) This theorem states that for any type `X` with a topological space structure and any type `α`, given a finite set `s` of `α` and a function `f` that maps each element of `α` to an open set in `X`, if every set `f i` for `i` in `s` is open, then the intersection of all such sets `f i` (i.e., the set `⋂ i ∈ s, f i`) is also open. In other words, it states that the intersection of a finite number of open sets is also an open set in a topological space. More concisely: In a topological space, the intersection of finitely many open sets is open.
`isOpen_iff_nhds` theorem isOpen_iff_nhds : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], IsOpen s ↔ ∀ x ∈ s, nhds x ≤ Filter.principal s This theorem states that for any type `X` and set `s` of `X` in a given topological space, `s` is an open set if and only if for every element `x` in `s`, the neighborhood filter of `x` is less than or equal to the principal filter of `s`. In other words, a set is open in a topological space if for all of its points, every neighborhood of that point contains the set, or equivalently, the set is a subset of all neighborhoods of each of its points. More concisely: A set `s` of a topological space is open if and only if for every `x` in `s`, the neighborhood filter of `x` contains the principal filter of `s`.
`IsOpen.interior_eq` theorem IsOpen.interior_eq : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], IsOpen s → interior s = s := by sorry The theorem `IsOpen.interior_eq` states that for any set `s` of type `X` in a topological space, if `s` is an open set, then the interior of `s` is equal to `s` itself. In other words, in a topological space, the interior of an open set is the set itself. This theorem is central to the concept of open sets in topology, where the interior of a set is defined as the largest open subset of the set. More concisely: In a topological space, an open set is equal to its interior.
`tendsto_nhds_limUnder` theorem tendsto_nhds_limUnder : ∀ {X : Type u} {α : Type u_1} [inst : TopologicalSpace X] {f : Filter α} {g : α → X} (h : ∃ x, Filter.Tendsto g f (nhds x)), Filter.Tendsto g f (nhds (limUnder f g)) The theorem `tendsto_nhds_limUnder` states that for any types `X` and `α`, where `X` is a topological space, any filter `f` in `α`, and any function `g` from `α` to `X`, if `g` tends to some neighborhood of a point `x` along `f` (meaning for every neighborhood of `x`, the pre-image under `g` is a neighborhood in the filter `f`), then `g` also tends to the neighborhood of the limit of `g` at `f`. This theorem is formulated with a nonempty `X` argument of limit derived from `h` to make it applicable to types without a nonempty `X` instance. Lean will unify this instance with any other due to built-in proof irrelevance. More concisely: If a function `g` from a filter `f` in `α` to a topological space `X` tends to a neighborhood of a point `x` in `X` along `f`, then `g` tends to the neighborhood of the limit of `g` at `f`.
`frontier_univ` theorem frontier_univ : ∀ {X : Type u} [inst : TopologicalSpace X], frontier Set.univ = ∅ The theorem `frontier_univ` states that for any type `X` with a topological space structure, the frontier of the universal set is the empty set. In other words, there are no points in `X` that lie between the closure and interior of the universal set, which consists of all elements in `X`. This is consistent with the intuition that the frontier of a space, which represents boundary points, should be empty in the case of the whole space. More concisely: The frontier of the universal set in any topological space is the empty set.
`interior_subset_closure` theorem interior_subset_closure : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], interior s ⊆ closure s := by sorry The theorem `interior_subset_closure` states that for any set `s` in a given topological space `X`, the interior of `s` is a subset of the closure of `s`. This is a fundamental theorem in topology that connects two important concepts: the interior of a set, which is the largest open subset contained within `s`, and the closure of a set, which is the smallest closed set containing `s`. The theorem, thus, provides a relationship between the 'open' and 'closed' aspects of a topological space. More concisely: The interior of a set is contained in its closure.
`isOpen_iInter_of_finite` theorem isOpen_iInter_of_finite : ∀ {X : Type u} {ι : Sort w} [inst : TopologicalSpace X] [inst_1 : Finite ι] {s : ι → Set X}, (∀ (i : ι), IsOpen (s i)) → IsOpen (⋂ i, s i) This theorem, `isOpen_iInter_of_finite`, states that for any type `X` with a given topological space structure, and for any finite index type `ι`, if we have a family of sets `s` indexed by `ι`, then if every set `s i` in this family is open in the topological space `X`, the intersection of all these sets `⋂ i, s i` is also open in `X`. In other words, the intersection of a finite collection of open sets in a topological space is also an open set. More concisely: The intersection of a finite collection of open sets in a topological space is open.
`dense_iff_inter_open` theorem dense_iff_inter_open : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], Dense s ↔ ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty This theorem states that, for any type `X` and any set `s` of type `X` within a topological space, the set `s` is dense if and only if for every set `U` of type `X`, if `U` is open and `U` is not empty, then the intersection of `U` and `s` is also not empty. In the context of topology, this essentially means that a set is dense if it intersects with every nonempty open set in the topological space. More concisely: A set `s` of type `X` in a topological space is dense if and only if the intersection of `s` and every nonempty open set `U` is not empty.
`Filter.HasBasis.lift'_closure` theorem Filter.HasBasis.lift'_closure : ∀ {X : Type u} {ι : Sort w} [inst : TopologicalSpace X] {l : Filter X} {p : ι → Prop} {s : ι → Set X}, l.HasBasis p s → (l.lift' closure).HasBasis p fun i => closure (s i) This theorem, `Filter.HasBasis.lift'_closure`, is about filters and topological spaces. It states that for any type `X` and index type `ι`, given a topological space over `X`, a filter `l` on `X`, a predicate `p` on `ι`, and a function `s` from `ι` to sets of `X`, if filter `l` has a basis defined by the predicate `p` and the function `s`, then the filter obtained by lifting `l` along the `closure` function (which transforms each set to its closure in the topological space) also has a basis defined by the same predicate `p` but with the function `s` now mapping each index to the closure of the corresponding set. In other words, the theorem demonstrates how the operation of taking closures of sets interacts nicely with the operation of lifting a filter along a function. More concisely: If a filter on a topological space has a basis given by a predicate and a function, then the filtered subsets generated by the closure of each set in the basis form a basis for the filtered subsets obtained by lifting the filter along the closure function.
`isClosed_iInter` theorem isClosed_iInter : ∀ {X : Type u} {ι : Sort w} [inst : TopologicalSpace X] {f : ι → Set X}, (∀ (i : ι), IsClosed (f i)) → IsClosed (⋂ i, f i) This theorem, named `isClosed_iInter`, states that for any type `X` with a topology, and any indexed collection of sets `{f : ι → Set X}`, if each set `f i` is closed, then the intersection of all these sets (denoted by `⋂ i, f i`) is also closed. In the context of topology, a set is said to be closed if its complement is an open set. The indexed collection is represented by a function `f` from the index set `ι` to the set of subsets of `X`. This theorem generalizes the idea that the intersection of a finite number of closed sets is also closed, to possibly infinite collections of closed sets. More concisely: If `X` is a topological space and `f : ι → Set X` is a family of closed sets, then the intersection `⋂ i, f i` is also closed.
`Dense.inter_of_isOpen_left` theorem Dense.inter_of_isOpen_left : ∀ {X : Type u} {s t : Set X} [inst : TopologicalSpace X], Dense s → Dense t → IsOpen s → Dense (s ∩ t) This theorem states that in any topological space `X`, if we have two sets `s` and `t` such that both are dense in `X` and `s` is an open set, then the intersection of `s` and `t` is also a dense set in `X`. In other words, every point in the topological space `X` belongs to the closure of the intersection of `s` and `t`. Here, a set is dense if every point in the space is either in the set or in the closure of the set, and a set is open if it belongs to the topology (it's one of the sets in the collection that defines the topological structure). More concisely: In any topological space, if two dense sets intersect and one is open, their intersection is also dense.
`mem_closure_iff_nhdsWithin_neBot` theorem mem_closure_iff_nhdsWithin_neBot : ∀ {X : Type u} {x : X} {s : Set X} [inst : TopologicalSpace X], x ∈ closure s ↔ (nhdsWithin x s).NeBot The theorem `mem_closure_iff_nhdsWithin_neBot` states that for any type `X` with a topology and any set `s` of elements of type `X`, an element `x` of type `X` is in the closure of `s` if and only if the "neighborhood within" filter of `x` and `s`, denoted as `nhdsWithin x s`, is not a bottom filter. In other words, `x` belongs to the smallest closed set containing `s` precisely when there exists a neighborhood of `x` within `s`. More concisely: An element x belongs to the closure of a set s if and only if there exists a neighborhood of x contained in s that does not contain the bottom filter.
`le_nhds_iff` theorem le_nhds_iff : ∀ {X : Type u} {x : X} [inst : TopologicalSpace X] {f : Filter X}, f ≤ nhds x ↔ ∀ (s : Set X), x ∈ s → IsOpen s → s ∈ f The theorem `le_nhds_iff` states that for any topological space `X`, any point `x` in `X`, and any filter `f` on `X`, the filter `f` is less than or equal to the neighborhood filter at `x` if and only if for every set `s` such that `x` is an element of `s` and `s` is open, `s` is an element of the filter `f`. In other words, a filter is subsumed by the neighborhood filter of a point if it contains every open set that contains that point. More concisely: A filter on a topological space is contained in the neighborhood filter of a point if and only if it contains every open set containing that point.
`Dense.mono` theorem Dense.mono : ∀ {X : Type u} {s₁ s₂ : Set X} [inst : TopologicalSpace X], s₁ ⊆ s₂ → Dense s₁ → Dense s₂ := by sorry The theorem `Dense.mono` states that for any type `X`, and for any two sets `s₁` and `s₂` of `X` under a given topology, if `s₁` is a subset of `s₂` and `s₁` is dense in the topological space, then `s₂` is also dense in the same topological space. In other words, the denseness property of a set is preserved under taking supersets in the same topology. More concisely: If `s₁ ⊆ s₂` and `s₁` is dense in the topological space `X`, then `s₂` is also dense in `X`.
`Set.MapsTo.closure` theorem Set.MapsTo.closure : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X} {t : Set Y}, Set.MapsTo f s t → Continuous f → Set.MapsTo f (closure s) (closure t) The given theorem states that if there exists a continuous map `f` from a set `s` to a set `t`, then this map `f` also maps the closure of `s` to the closure of `t`. In other words, under a continuous map, the closure of a set is mapped to the closure of its image. Here, `Set.MapsTo f s t` means that the image of `s` under `f` is contained in `t`, `closure s` and `closure t` denote the smallest closed sets containing `s` and `t` respectively, and `Continuous f` means that the function `f` is continuous. More concisely: If `f` is a continuous function from a set `s` to a set `t` in Lean 4, then the closure of `s` is mapped to the closure of `t`, that is, `closure (Image f s) = Image (closure f) (closure s)`.
`IsClosed.closure_eq` theorem IsClosed.closure_eq : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], IsClosed s → closure s = s := by sorry This theorem states that for any type `X` and any set `s` of `X`, in the context of a topological space given by `inst`, if `s` is a closed set, then the closure of `s` is equal to `s` itself. In other words, the closure of a closed set in a topological space is the set itself. In mathematical terms, if `s` is a closed set in a topological space, then the intersection of all closed sets that contain `s` (the closure of `s`) is just `s`. More concisely: A closed set in a topological space is equal to its closure.
`mem_closure_iff_nhds_neBot` theorem mem_closure_iff_nhds_neBot : ∀ {X : Type u} {x : X} {s : Set X} [inst : TopologicalSpace X], x ∈ closure s ↔ nhds x ⊓ Filter.principal s ≠ ⊥ This theorem states that for any type `X`, given an element `x` of `X`, a set `s` of `X` elements and a topological space structure on `X` (denoted as `inst`), `x` is in the closure of `s` if and only if the intersection of the neighborhood filter at `x` and the principal filter of `s` is not the bottom element (`⊥` representing the empty set in the context of filters). In simpler terms, the theorem says that a point is in the closure of a set if and only if every neighborhood of the point intersects the set. More concisely: A point x in a topological space X belongs to the closure of a set s if and only if the neighborhood filter of x intersects the principal filter of s is non-empty.
`Filter.EventuallyEq.eventuallyEq_nhds` theorem Filter.EventuallyEq.eventuallyEq_nhds : ∀ {X : Type u} {α : Type u_1} {x : X} [inst : TopologicalSpace X] {f g : X → α}, (nhds x).EventuallyEq f g → ∀ᶠ (y : X) in nhds x, (nhds y).EventuallyEq f g This theorem states that if two functions are equal in a neighborhood of a point `x` (in a topological space `X`), then for each point `y` in a neighborhood around `x`, the two functions are also equal in a neighborhood around `y`. In mathematical terms, it means that if `f` and `g` are two functions from `X` to any type `α` such that `f` and `g` are equal at a vicinity of a point `x` (expressed as `f =ᶠ[nhds x] g`), then for almost every point `y` in the vicinity of `x` (expressed as `∀ᶠ (y : X) in nhds x`), `f` and `g` are also equal in the vicinity of `y` (expressed as `f =ᶠ[nhds y] g`). More concisely: If functions $f$ and $g$ are equal in a neighborhood of a point $x$ in a topological space, then they are equal in the neighborhoods of almost all points $y$ around $x$.
`isOpen_empty` theorem isOpen_empty : ∀ {X : Type u} [inst : TopologicalSpace X], IsOpen ∅ The theorem `isOpen_empty` states that for any type `X` equipped with a topological space structure, the empty set is open in this topological space. In mathematical terms, this theorem asserts that in any topological space, the empty set is always an open set, which is a fundamental axiom of topology. More concisely: In any topological space, the empty set is an open set.
`isClosed_iff_frequently` theorem isClosed_iff_frequently : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], IsClosed s ↔ ∀ (x : X), (∃ᶠ (y : X) in nhds x, y ∈ s) → x ∈ s A set `s` is said to be closed if and only if for every point `x` in the topological space `X`, if there exists a frequently occurring point `y` in the neighborhood of `x` that belongs to `s`, then `x` also belongs to `s`. This theorem serves as a condition for determining the closed nature of a set in a topological space. The neighborhood of a point is defined in terms of a filter representing a collection of all open sets containing the point. More concisely: A set in a topological space is closed if for every point in the set's boundary and every frequently occurring point in a neighborhood of that point that belongs to the set, the original point also belongs to the set.
`frontier_subset_closure` theorem frontier_subset_closure : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], frontier s ⊆ closure s := by sorry This theorem states that for any given type `X` and a set `s` of type `X` in a topological space, the frontier of the set `s` is a subset of the closure of the set `s`. The frontier of a set is defined as the set of points lying between the closure and interior of a set, while the closure of a set is the smallest closed set that contains the set. This theorem establishes a basic property of frontiers and closures in topological spaces. More concisely: The theorem asserts that the frontier of a set is a subset of its closure in a topological space.
`DenseRange.comp` theorem DenseRange.comp : ∀ {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace Z] {α : Type u_4} {g : Y → Z} {f : α → Y}, DenseRange g → DenseRange f → Continuous g → DenseRange (g ∘ f) This theorem states that for any types `Y`, `Z`, and `α`, and given two functions `g : Y → Z` and `f : α → Y`, if `g` has a dense range in `Z` and `f` has a dense range in `Y`, and if `g` is a continuous function, then the composition of `g` and `f` (denoted as `g ∘ f`) also has a dense range. Here, a function having a dense range means that its image is a dense subset in the codomain, and a set is dense in a topological space if every point in the space is either in the set or is a limit point of the set. More concisely: If functions `g : Y → Z` and `f : α → Y` are continuous, have dense ranges, and `g` maps `Y` onto a dense subset of `Z`, then `g ∘ f` also has a dense range in `Z`.
`acc_principal_iff_cluster` theorem acc_principal_iff_cluster : ∀ {X : Type u} [inst : TopologicalSpace X] (x : X) (C : Set X), AccPt x (Filter.principal C) ↔ ClusterPt x (Filter.principal (C \ {x})) The theorem `acc_principal_iff_cluster` states that for any type `X` that is equipped with a topology, and for any given `x` of type `X` and a set `C` of elements of type `X`, `x` is an accumulation point of the set `C` if and only if `x` is a cluster point of the set obtained by removing `x` from `C`. In other words, an element is an accumulation point of a set if and only if it is a cluster point of the set excluding the element itself. In terms of topological spaces, an accumulation point is a point where every neighborhood of the point (excluding the point itself) intersects the set, while a cluster point is a point where every neighborhood of the point (including the point) intersects the set. Therefore, this theorem is expressing a relationship between these two types of special points in a set within a topological space. More concisely: An element is an accumulation point of a set if and only if it is a cluster point of the set without that element.
`Filter.HasBasis.lift'_closure_eq_self` theorem Filter.HasBasis.lift'_closure_eq_self : ∀ {X : Type u} {ι : Sort w} [inst : TopologicalSpace X] {l : Filter X} {p : ι → Prop} {s : ι → Set X}, l.HasBasis p s → (∀ (i : ι), p i → IsClosed (s i)) → l.lift' closure = l The theorem `Filter.HasBasis.lift'_closure_eq_self` states that for any type `X` with a topological space structure, for any filter `l` on `X`, and for any collection of subsets `s` of `X` indexed by `ι` such that `l` has a basis given by the properties `p` and the sets `s` (i.e., `Filter.HasBasis l p s`), if all subsets `s i` satisfying the property `p i` are closed, then lifting the filter `l` using the closure operation yields the same filter `l`. In other words, the closure operation does not change the filter when it is formed from a basis of closed sets. More concisely: Let `(X, top)` be a topological space, `l` be a filter on `X` with basis `s : ι → Set X` such that `s i` is closed for all `i` with property `p i`, then `l = Filter.closure l (Filter.union (map (closure) s))`.
`continuous_id'` theorem continuous_id' : ∀ {X : Type u_1} [inst : TopologicalSpace X], Continuous fun x => x This theorem states that for any type `X` equipped with a topology (denoted by `TopologicalSpace X`), the identity function (defined as `fun x => x`) is continuous. In mathematical terms, for all topological spaces, the identity mapping is always continuous. More concisely: The identity function is continuous on any topological space.
`IsOpen.inter_closure` theorem IsOpen.inter_closure : ∀ {X : Type u} {s t : Set X} [inst : TopologicalSpace X], IsOpen s → s ∩ closure t ⊆ closure (s ∩ t) The theorem `IsOpen.inter_closure` states that for any type `X`, given two sets `s` and `t` of `X` in a topological space, if `s` is an open set, then the intersection of `s` and the closure of `t` is a subset of the closure of the intersection of `s` and `t`. Here, the closure of a set is the smallest closed set that contains it. It essentially says that the intersection of an open set with a closure of another set is contained within the closure of the intersection of those two sets. More concisely: For any topological space `X` and open set `s` in `X`, and sets `t` and `cl(t)` in `X` where `cl(t)` is the closure of `t`, we have `s ∩ cl(t) ⊆ cl(s ∩ t)`.
`DenseRange.dense_of_mapsTo` theorem DenseRange.dense_of_mapsTo : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {f : X → Y}, DenseRange f → Continuous f → Dense s → ∀ {t : Set Y}, Set.MapsTo f s t → Dense t The theorem `DenseRange.dense_of_mapsTo` states that for any two types `X` and `Y` equipped with topological spaces, a set `s` of type `X`, and a function `f` mapping `X` to `Y`, if `f` has a dense range, `f` is continuous, and `s` is a dense set, then for any set `t` of type `Y`, if `f` maps the set `s` to a subset of `t`, then `t` is a dense set. In more mathematical terms, this theorem is saying that the image of a dense set under a continuous function with dense range is a dense set. More concisely: If a continuous function with dense range maps a dense set to a subset of another set, then the latter set is dense.
`continuousAt_congr` theorem continuousAt_congr : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {x : X} {g : X → Y}, (nhds x).EventuallyEq f g → (ContinuousAt f x ↔ ContinuousAt g x) This theorem states that for any two functions `f` and `g` from a topological space `X` to another topological space `Y`, if the functions `f` and `g` are locally equal at a point `x` (i.e., `f` equals `g` at every point in a neighborhood of `x`), then the continuity of `f` at `x` is equivalent to the continuity of `g` at `x`. In other words, if two functions agree in a neighborhood of a point, then either both are continuous at that point or both are not. More concisely: If two functions between topological spaces are locally equal at a point, then their continuity at that point are equivalent.
`isOpen_interior` theorem isOpen_interior : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], IsOpen (interior s) The theorem `isOpen_interior` states that for any type `X` and any set `s` of type `X`, given that a topological structure `inst` is defined on `X`, the interior of set `s` is an open set in this topological space. In other words, in any given topological space, the interior of any set is always an open set. This is a fundamental property in topology, and is universally true regardless of the specific details of the topological space or the set. More concisely: In any topological space, the interior of a set is an open set.
`le_nhds_lim` theorem le_nhds_lim : ∀ {X : Type u} [inst : TopologicalSpace X] {f : Filter X} (h : ∃ x, f ≤ nhds x), f ≤ nhds (lim f) This theorem states that given a filter `f` in a topological space `X` such that there exists an element `x` in `X` for which the filter `f` is majorated by the neighborhood filter at `x` (meaning that `f` is contained in `nhds x`), then this filter `f` is also majorated by the neighborhood filter at `Filter.lim f` (the limit of filter `f`). The theorem requires that `X` is nonempty, with the nonemptiness derived from `h`. This is written in a way that makes it usable for types that don't already have a `Nonempty X` instance. Due to proof irrelevance in Lean, this instance will be congruent with any other instance. More concisely: If a filter `f` in a nonempty topological space `X` is majorated by the neighborhood filter of an element `x` in `X`, then `f` is majorated by the neighborhood filter of the limit of `f`.
`interior_mono` theorem interior_mono : ∀ {X : Type u} {s t : Set X} [inst : TopologicalSpace X], s ⊆ t → interior s ⊆ interior t := by sorry This theorem, named `interior_mono`, states that for any type `X` with a topology (that is, `X` is a topological space), and for any two sets `s` and `t` of elements of type `X`, if `s` is a subset of `t`, then the interior of `s` is also a subset of the interior of `t`. The interior of a set is defined as the largest open subset of the given set, in the context of the topology on `X`. So, this theorem establishes a monotonicity property for the operation of taking interiors of sets in a topological space. More concisely: If `X` is a topological space and `s` is a subset of `t`, then the interior of `s` is contained in the interior of `t`.
`map_mem_closure` theorem map_mem_closure : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X} {x : X} {t : Set Y}, Continuous f → x ∈ closure s → Set.MapsTo f s t → f x ∈ closure t This theorem states that for any types `X` and `Y` with respective topological spaces, any function `f` from `X` to `Y`, any set `s` of type `X`, any element `x` of type `X`, and any set `t` of type `Y`; if `f` is continuous, `x` is in the closure of `s`, and `f` maps elements of `s` to `t`, then `f(x)` is in the closure of `t`. In other words, the image under a continuous function of a point in the closure of a set is in the closure of the image of that set. This is a property linking continuity, closure of sets, and the mapping of sets under functions in topological spaces. More concisely: If a continuous function maps a point in the closure of a set to a set, then the image of that point is in the closure of the image of the set.
`disjoint_interior_frontier` theorem disjoint_interior_frontier : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], Disjoint (interior s) (frontier s) The theorem `disjoint_interior_frontier` states that for any given set `s` in a topological space `X`, the interior and the frontier of the set `s` are disjoint. In other words, there are no common elements between the interior and the frontier of the set. The interior of a set is the largest open subset of the set, while the frontier of a set is the set of points between the closure and the interior of the set. The disjointness in this context means that the intersection of the interior and the frontier is the bottom element (empty set) in the lattice of sets of `X`. More concisely: The interior and frontier of a set in a topological space are disjoint, i.e., their intersection is the empty set.
`ContinuousAt.tendsto` theorem ContinuousAt.tendsto : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {x : X}, ContinuousAt f x → Filter.Tendsto f (nhds x) (nhds (f x)) The theorem `ContinuousAt.tendsto` states that for all types `X` and `Y` endowed with topological space structure, and for any function `f` from `X` to `Y` and any point `x` in `X`, if `f` is continuous at `x`, then `f` has the property that for every neighborhood of `f(x)`, the pre-image under `f` of that neighborhood is a neighborhood of `x`. This is essentially stating that the limit of `f` at `x` in the source topological space equals `f(x)` in the target topological space, which is a generic way of expressing the concept of continuity in topology. More concisely: If `f` is a continuous function from a topological space `X` to a topological space `Y` at a point `x` in `X`, then for every neighborhood `V` of `f(x)` in `Y`, there exists a neighborhood `U` of `x` in `X` such that `f(U)` is a subset of `V`.
`Mathlib.Topology.Basic._auxLemma.19` theorem Mathlib.Topology.Basic._auxLemma.19 : ∀ {X : Type u} [inst : TopologicalSpace X] (s : Set X), (closure s = ∅) = (s = ∅) This theorem states that for any given set `s` in a topological space `X`, the closure of `s` is empty, denoted as `closure s = ∅`, if and only if `s` itself is empty, expressed as `s = ∅`. In other words, the theorem establishes the equivalence between the condition of `s` being an empty set and its closure also being an empty set in a given topological space. More concisely: The closure of an empty set in a topological space is empty if and only if the original set is empty.
`closure_minimal` theorem closure_minimal : ∀ {X : Type u} {s t : Set X} [inst : TopologicalSpace X], s ⊆ t → IsClosed t → closure s ⊆ t The theorem `closure_minimal` states that for any type `X` with a topology (denoted by `inst : TopologicalSpace X`), and any two sets `s` and `t` of type `X`, if `s` is a subset of `t` and `t` is a closed set, then the closure of set `s` is also a subset of `t`. In other words, in a topological space, the closure of a set is always contained within any closed set that contains the original set. More concisely: If `s` is a subset of a closed set `t` in a topological space `X`, then the closure of `s` is contained in `t`.
`TopologicalSpace.ext_iff` theorem TopologicalSpace.ext_iff : ∀ {X : Type u} {t t' : TopologicalSpace X}, t = t' ↔ ∀ (s : Set X), IsOpen s ↔ IsOpen s The theorem `TopologicalSpace.ext_iff` states that for any given type `X` and any two topological spaces `t` and `t'` over `X`, `t` is equal to `t'` if and only if for every set `s` in `X`, `s` is open in `t` if and only if `s` is open in `t'`. In other words, two topological spaces on the same set are identical if they have the same open sets. More concisely: Two topological spaces over the same set are equal if and only if they have identical open sets.
`IsOpen.preimage` theorem IsOpen.preimage : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}, Continuous f → ∀ {t : Set Y}, IsOpen t → IsOpen (f ⁻¹' t) The theorem `IsOpen.preimage` states that for any types `X` and `Y` equipped with topological spaces, if `f` is a continuous function mapping from `X` to `Y`, then for any open set `t` in `Y`, the preimage of `t` under `f` is an open set in `X`. More concisely: If `f` is a continuous function from topological spaces `X` and `Y`, then for any open set `t` in `Y`, the preimage `f⁻¹(t)` is an open set in `X`.
`DenseRange.exists_mem_open` theorem DenseRange.exists_mem_open : ∀ {X : Type u_1} [inst : TopologicalSpace X] {α : Type u_4} {f : α → X} {s : Set X}, DenseRange f → IsOpen s → s.Nonempty → ∃ a, f a ∈ s The theorem `DenseRange.exists_mem_open` states that for any types `X` and `α` where `X` is equipped with a topological space structure, and for any function `f` from `α` to `X` and any set `s` of `X`, if `f` has a dense range and `s` is an open set in `X` that is not empty, then there exists an element `a` in `α` such that `f(a)` is an element of `s`. In other words, for every nonempty open set in the topological space, there is a point in the dense range of the function that lies within that open set. More concisely: For any continuous function `f` from a non-empty open set of a topological space `X` to `X` with a dense range, there exists an element `a` in the domain of `f` such that `f(a)` is in the open set.
`Dense.denseRange_val` theorem Dense.denseRange_val : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, Dense s → DenseRange Subtype.val This theorem states that for any type `X` with a topological space structure, and any set `s` of `X`, if `s` is dense in `X`, then the range of the function `Subtype.val` (which extracts the underlying element from a subtype) is also dense in `X`. In other words, if every point in `X` belongs to the closure of `s`, then every point in `X` also belongs to the closure of the image of `Subtype.val`. More concisely: If `s` is a dense subset of the topological space `X`, then the image of `Subtype.val` on `s` is also a dense subset of `X`.
`IsClosed.inter` theorem IsClosed.inter : ∀ {X : Type u} {s₁ s₂ : Set X} [inst : TopologicalSpace X], IsClosed s₁ → IsClosed s₂ → IsClosed (s₁ ∩ s₂) := by sorry The theorem `IsClosed.inter` states that for any type `X`, and any two sets `s₁` and `s₂` of type `X`, given a topology (or `TopologicalSpace`) on `X`, if both `s₁` and `s₂` are closed sets, then their intersection (expressed as `s₁ ∩ s₂`) is also a closed set in the given topological space. The theorem essentially formalizes one of the standard properties of topological spaces, namely that the intersection of any collection of closed sets is itself a closed set. More concisely: In a topological space, the intersection of any two closed sets is a closed set.
`Continuous.comp'` theorem Continuous.comp' : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z] {f : X → Y} {g : Y → Z}, Continuous g → Continuous f → Continuous fun x => g (f x) This theorem states that if you have three types `X`, `Y` and `Z`, each with a topological space structure, and two functions `f` from `X` to `Y`, and `g` from `Y` to `Z`, then if `g` and `f` are both continuous functions, the composition function `g ∘ f` (that is, the function that first applies `f`, then applies `g` to the result) is also continuous. This is a formalization of the standard mathematical fact about the composition of continuous functions in topology. More concisely: If `f` is a continuous function from `X` to `Y` and `g` is a continuous function from `Y` to `Z`, then the composition `g ∘ f` is a continuous function from `X` to `Z`.
`tendsto_inf_principal_nhds_iff_of_forall_eq` theorem tendsto_inf_principal_nhds_iff_of_forall_eq : ∀ {X : Type u} {α : Type u_1} {x : X} [inst : TopologicalSpace X] {f : α → X} {l : Filter α} {s : Set α}, (∀ a ∉ s, f a = x) → (Filter.Tendsto f (l ⊓ Filter.principal s) (nhds x) ↔ Filter.Tendsto f l (nhds x)) The theorem `tendsto_inf_principal_nhds_iff_of_forall_eq` states that for any types `X` and `α`, a topological space on `X`, a function `f` from `α` to `X`, a filter `l` on `α`, a set `s` of `α`, and a point `x` in `X`, if the function `f` maps all elements not in the set `s` to the point `x`, then the function `f` tends to the point `x` along the filter `l` restricted to the set `s` (represented as `l ⊓ Filter.principal s`) if and only if the function `f` tends to the point `x` along the filter `l`. In other words, restricting the filter `l` to the set `s` does not change the limit of the function `f` if `f` sends all points outside `s` to `x`. More concisely: For a function between types and a filter on a set, if the function maps elements not in the set to a fixed point and the limit of the function along the filter exists, then the limit along the restricted filter to the set is equal to the limit along the original filter.
`ClusterPt.of_le_nhds` theorem ClusterPt.of_le_nhds : ∀ {X : Type u} {x : X} [inst : TopologicalSpace X] {f : Filter X}, f ≤ nhds x → ∀ [inst_1 : f.NeBot], ClusterPt x f The theorem `ClusterPt.of_le_nhds` states that for any type `X` endowed with a topological space structure, any point `x` of type `X`, and any filter `f` on `X`, if `f` is less than or equal to the neighborhood filter at `x` and `f` is not the bottom filter, then `x` is a cluster point of `f`. In other words, if a filter `f` is contained within the neighborhood of a point `x` and `f` is not the trivial (empty) filter, then `x` is an accumulation point of `f`. Here, the neighborhood filter is the filter consisting of all neighborhoods of `x`, and a point is called a cluster point of a filter if the intersection of the neighborhood filter of the point and the filter is not the bottom filter. More concisely: If a filter on a topological space is contained in the neighborhood filter of a point and is not the bottom filter, then that point is a cluster point of the filter.
`isClosed_sInter` theorem isClosed_sInter : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set (Set X)}, (∀ t ∈ s, IsClosed t) → IsClosed s.sInter This theorem states that for any type `X` equipped with a topology, and for any set `s` of subsets of `X`, if every subset `t` in `s` is a closed set, then the intersection of all subsets in `s` is also a closed set. In mathematical terms, for any topological space `X` and any collection `s` of closed subsets of `X`, the intersection over `s` is closed. More concisely: Given a topological space `X` and a collection `s` of closed subsets of `X`, their intersection is also a closed subset of `X`.
`accPt_iff_frequently` theorem accPt_iff_frequently : ∀ {X : Type u} [inst : TopologicalSpace X] (x : X) (C : Set X), AccPt x (Filter.principal C) ↔ ∃ᶠ (y : X) in nhds x, y ≠ x ∧ y ∈ C The theorem `accPt_iff_frequently` states that for any type `X` with a topological space structure, and for any `x` of type `X` and `C` a set of type `X`, `x` is an accumulation point of the set `C` if and only if there are points arbitrarily close to `x` that are distinct from `x` and belong to `C`. In other words, it means that in the neighborhood of `x`, there are other points from set `C`, thus making `x` an accumulation point of `C`. The neighborhood of a point includes all points that are in some open set containing the point, excluding the point itself. More concisely: A point `x` in a topological space `X` is an accumulation point of a set `C` if and only if there exists a sequence `(x\_n)` in `C` distinct from `x` such that `x\_n` converges to `x`.
`IsClosed.mem_of_tendsto` theorem IsClosed.mem_of_tendsto : ∀ {X : Type u} {α : Type u_1} {x : X} {s : Set X} [inst : TopologicalSpace X] {f : α → X} {b : Filter α} [inst_1 : b.NeBot], IsClosed s → Filter.Tendsto f b (nhds x) → (∀ᶠ (x : α) in b, f x ∈ s) → x ∈ s This theorem states that, for every type `X` and `α`, any point `x` in `X`, and a set `s` of `X`, given a topological space structure on `X`, a function `f` from `α` to `X`, and a filter `b` on `α` which is not bottom, if `s` is a closed set, and the function `f` tends to the neighborhood filter of `x` as `b` tends to infinity (denoted by `Filter.Tendsto f b (nhds x)`), then if almost all elements `x` in `b` map to `s` under `f`, it follows that `x` is an element of `s`. In essence, this theorem is about the limit behavior of a function in a topological space and its relationship with closed sets. More concisely: Given a topological space `(X, top)`, a function `f : α -> X`, a point `x in X`, a filter `b on α` that is not bottom, and a closed set `s in X`, if `Filter.Tendsto f b (nhds x)` and `almost_all x in b are in s`, then `x is in s`.
`interior_eq_nhds'` theorem interior_eq_nhds' : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], interior s = {x \| s ∈ nhds x} := by sorry This theorem states that for any type `X` and any set `s` of type `Set X` in a topological space, the interior of `s` is equal to the set of all elements `x` such that `s` is a neighborhood of `x`. In simpler terms, it asserts that the interior of a set consists of all points which have a neighborhood completely contained within the set. This theorem provides a link between the concepts of the interior of a set and neighborhood filters in a topological space. More concisely: The interior of a set in a topological space is equal to the set of all points that have the set as their neighborhood.
`tendsto_atTop_of_eventually_const` theorem tendsto_atTop_of_eventually_const : ∀ {X : Type u} {x : X} [inst : TopologicalSpace X] {ι : Type u_3} [inst_1 : SemilatticeSup ι] [inst_2 : Nonempty ι] {u : ι → X} {i₀ : ι}, (∀ i ≥ i₀, u i = x) → Filter.Tendsto u Filter.atTop (nhds x) The theorem `tendsto_atTop_of_eventually_const` asserts that for any type `X` with a topology, a type `ι` with a semilattice structure and a nonempty property, a function `u` mapping from `ι` to `X`, an element `x` in `X` and an element `i₀` in `ι`, if for all `i` greater than or equal to `i₀`, `u i` equals `x`, then the function `u` tends to `x` at infinity (i.e., the limit of `u` as `i` approaches infinity in `ι` is `x`). In other words, if a function is constant after some point, then the limit of the function at infinity is the constant value. More concisely: If a function from an ordered index type with a semilattice structure to a topological space is constant after some index, then the function converges to that constant value at infinity.
`dense_univ` theorem dense_univ : ∀ {X : Type u} [inst : TopologicalSpace X], Dense Set.univ The theorem `dense_univ` states that for any type `X` with a topology, the universal set of `X` is dense. This means that in any topological space, every point belongs to the closure of the universal set, which includes all elements of the space. In other words, there's no point in the space that isn't arbitrarily close to some element of the universal set. More concisely: In any topological space, the universal set is dense, meaning every point belongs to the closure of the universal set.
`dense_compl_singleton` theorem dense_compl_singleton : ∀ {X : Type u} [inst : TopologicalSpace X] (x : X) [inst_1 : (nhdsWithin x {x}ᶜ).NeBot], Dense {x}ᶜ The theorem `dense_compl_singleton` states that for any topological space `X` and any point `x` in `X`, if `x` is not an isolated point (which means that every neighborhood of `x` contains other points than `x` itself), then the set of all points in `X` excluding `x` (denoted by `{x}ᶜ`) is dense in `X`. In mathematical terms, every point in `X` is either in `{x}ᶜ` or it is a limit point of `{x}ᶜ`, i.e., every neighborhood of the point contains a point from `{x}ᶜ`. More concisely: If a point in a topological space is not isolated, then the complement of that point is dense in the space.
`Dense.of_closure` theorem Dense.of_closure : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], Dense (closure s) → Dense s := by sorry This theorem, named `Dense.of_closure`, states that given a type `X` and a set `s` of type `X` in a topological space, if the closure of set `s` is dense, then the set `s` itself is also dense. In other words, if every point in the topological space belongs to the closure of `s`, then every point also belongs to `s`. It implies that denseness is preserved under the operation of taking closures in a topological space. More concisely: If a set `s` in a topological space is dense if and only if its closure is dense.
`Dense.closure_eq` theorem Dense.closure_eq : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], Dense s → closure s = Set.univ := by sorry This theorem, referred to as `Dense.closure_eq`, states that for any type `X` and any set `s` of that type, in the context of a topological structure over `X`, if the set `s` is dense in that topology, then the closure of `s` is equal to the universal set. In other words, when a set is dense in a given topological space, the smallest closed set that contains all its elements coincides with the set of all elements in the space. More concisely: In a topological space, if a set is dense then its closure is equal to the universal set.
`frontier_compl` theorem frontier_compl : ∀ {X : Type u} [inst : TopologicalSpace X] (s : Set X), frontier sᶜ = frontier s This theorem states that, for any set in a topological space, the frontier of the complement of the set is the same as the frontier of the set itself. Here, the 'frontier' of a set is defined as the set of points that lie between the closure and the interior of the set. The 'complement' of a set consists of all points that are not in the set. Hence, in more plain terms, the boundary of a set and the boundary of everything not in the set are the same. More concisely: The boundary of a set in a topological space is equal to the boundary of its complement.
`subset_interior_iff_isOpen` theorem subset_interior_iff_isOpen : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], s ⊆ interior s ↔ IsOpen s This theorem states that for any type `X` and any set `s` of type `X` in a given topological space, the set `s` is a subset of its interior if and only if the set `s` is open. In terms of topology, this means that a set is open (i.e., each point in the set is an interior point) if and only if all of its points are interior points, which is true by definition of an open set. More concisely: A set `s` of type `X` in a topological space is equal to its interior if and only if it is open.
`isOpen_iUnion` theorem isOpen_iUnion : ∀ {X : Type u} {ι : Sort w} [inst : TopologicalSpace X] {f : ι → Set X}, (∀ (i : ι), IsOpen (f i)) → IsOpen (⋃ i, f i) The theorem `isOpen_iUnion` states that for any type `X` with a topological space structure, and any indexing type `ι`, if you have a function `f` from `ι` to the sets of `X` such that for each index `i` the set `f i` is open, then the union of all these sets `(⋃ i, f i)` is also an open set in `X`. In other words, in a topological space, the arbitrary union of open sets is again an open set. More concisely: In a topological space, the union of any family of open sets is an open set.
`IsClosed.union` theorem IsClosed.union : ∀ {X : Type u} {s₁ s₂ : Set X} [inst : TopologicalSpace X], IsClosed s₁ → IsClosed s₂ → IsClosed (s₁ ∪ s₂) := by sorry This theorem asserts that for any type `X` with a topology (`TopologicalSpace X`), if `s₁` and `s₂` are closed sets (`IsClosed s₁` and `IsClosed s₂`), then their union `s₁ ∪ s₂` is also a closed set (`IsClosed (s₁ ∪ s₂)`). In mathematical terms, this theorem is stating the common property of topological spaces where the union of two closed sets is again a closed set. More concisely: In a topological space, the union of two closed sets is closed.
`TopologicalSpace.ext_isClosed` theorem TopologicalSpace.ext_isClosed : ∀ {X : Type u} {t₁ t₂ : TopologicalSpace X}, (∀ (s : Set X), IsClosed s ↔ IsClosed s) → t₁ = t₂ This theorem, also known as the Alias of the reverse direction of `TopologicalSpace.ext_iff_isClosed`, asserts that for any type `X` and any two topological spaces `t₁` and `t₂` on `X`, if for every set `s` of `X`, `s` is closed in `t₁` if and only if `s` is closed in `t₂`, then `t₁` and `t₂` must be the same topological space. In terms of topology, this theorem states that two topological spaces are identical if they agree on the closure of all subsets. More concisely: Two topological spaces on a set are equal if they have the same closed sets.
`isClosed_univ` theorem isClosed_univ : ∀ {X : Type u} [inst : TopologicalSpace X], IsClosed Set.univ This theorem states that for any type `X` equipped with a topology (that is, `X` is taken to be a topological space), the universal set (i.e., the set containing all elements of `X`) is a closed set. In mathematical terms, this represents the universally true fact that in any given topological space, the entire space itself is always considered a closed set. More concisely: In any topological space, the universal set is closed.
`continuous_def` theorem continuous_def : ∀ {X : Type u_1} {Y : Type u_2} {x : TopologicalSpace X} {x_1 : TopologicalSpace Y} {f : X → Y}, Continuous f ↔ ∀ (s : Set Y), IsOpen s → IsOpen (f ⁻¹' s) This theorem states that a function `f` between two topological spaces `X` and `Y` is continuous if and only if for every set `s` in `Y` that is open in the topological space of `Y`, the preimage of `s` under `f` is open in the topological space of `X`. In other words, the continuity of a function is defined by the property that the preimage of an open set is always open. More concisely: A function between two topological spaces is continuous if and only if the preimage of every open set is open.
`isOpen_iff_mem_nhds` theorem isOpen_iff_mem_nhds : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], IsOpen s ↔ ∀ x ∈ s, s ∈ nhds x The theorem `isOpen_iff_mem_nhds` states that for any Type `X` and any set `s` of type `X` in a given topological space, `s` is open if and only if for every element `x` in `s`, `s` is a neighborhood of `x`. In other words, a set is open in a topological space if and only if for all elements of the set, the set is a neighborhood of each of its elements. More concisely: A set in a topological space is open if and only if it is a neighborhood of each of its elements.
`ContinuousAt.comp_of_eq` theorem ContinuousAt.comp_of_eq : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z] {f : X → Y} {x : X} {y : Y} {g : Y → Z}, ContinuousAt g y → ContinuousAt f x → f x = y → ContinuousAt (g ∘ f) x The theorem named "ContinuousAt.comp_of_eq" states the following: Given three types `X`, `Y`, and `Z`, each equipped with a topological space structure, along with a function `f` from `X` to `Y`, a function `g` from `Y` to `Z`, and elements `x` of `X` and `y` of `Y`. If `g` is continuous at `y`, `f` is continuous at `x`, and `f(x)` equals `y`, then the composition `g ∘ f` is continuous at `x`. This can be interpreted as follows: if we have a chain of mappings where each mapping is continuous at the corresponding point, then the entire chain also preserves the property of continuity at the source point. More concisely: If functions `f : X → Y`, `g : Y → Z`, `x ∈ X`, `y ∈ Y` with `y = f x` and `g` continuous at `y` imply `g ∘ f` is continuous at `x`, then continuity is preserved under composition.
`exists_open_set_nhds'` theorem exists_open_set_nhds' : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X] {U : Set X}, U ∈ ⨆ x ∈ s, nhds x → ∃ V, s ⊆ V ∧ IsOpen V ∧ V ⊆ U This theorem states that for any type `X` with a topological space structure, if a set `U` is a neighborhood of each point of another set `s`, then `U` itself is a neighborhood of `s`. In other words, `U` contains an open set `V` that contains `s`. Here, the term "neighborhood" implies that `U` contains an open set around each point in `s`, and "open" is in the context of the topological space on `X`. The theorem formally asserts that if `U` belongs to the filter generated by the neighborhood filters of each point in `s`, then there exists an open set `V` such that `s` is a subset of `V`, `V` is open, and `V` is a subset of `U`. More concisely: If a set `U` is a neighborhood of each point in another set `s` in a topological space, then there exists an open set `V` contained in `U` that contains `s`.
`closure_univ` theorem closure_univ : ∀ {X : Type u} [inst : TopologicalSpace X], closure Set.univ = Set.univ This theorem states that for any type `X` endowed with a topology (i.e., `X` has a topological space structure), the closure of the universal set is the universal set itself. In mathematical terms, given any topological space `X`, the smallest closed set that contains all elements of `X` (the closure of the universal set) is just the set of all elements of `X` (the universal set). This result is expected because the universal set, containing all elements, is inherently closed, so its closure doesn't have to include any additional elements. More concisely: In a topological space, the closure of the universal set is equivalent to the universal set itself.
`Continuous.tendsto` theorem Continuous.tendsto : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}, Continuous f → ∀ (x : X), Filter.Tendsto f (nhds x) (nhds (f x)) The theorem `Continuous.tendsto` states that for all types `X` and `Y`, given topological spaces over `X` and `Y`, and a function `f` from `X` to `Y`, if the function `f` is continuous, then for all `x` in `X`, `f` tends to the neighborhood filter of `f(x)` when the input tends to the neighborhood filter of `x`. In essence, this theorem formulates the property that a function is continuous at a point if and only if the pre-image of any neighborhood of the function's value at that point contains a neighborhood of the point. More concisely: A continuous function from a topological space X to a topological space Y sends the neighborhood filter of any point x in X to the neighborhood filter of f(x) in Y.

LeanAide GPT-4 documentation

Module: Mathlib.Topology.Basic

nhds_le_of_le

theorem nhds_le_of_le : ∀ {X : Type u} {x : X} {s : Set X} [inst : TopologicalSpace X] {f : Filter X}, x ∈ s → IsOpen s → Filter.principal s ≤ f → nhds x ≤ f

isClosed_compl_iff

theorem isClosed_compl_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsClosed sᶜ ↔ IsOpen s

interior_empty

theorem interior_empty : ∀ {X : Type u} [inst : TopologicalSpace X], interior ∅ = ∅

continuous_id

theorem continuous_id : ∀ {X : Type u_1} [inst : TopologicalSpace X], Continuous id

closure_subset_iff_isClosed

theorem closure_subset_iff_isClosed : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], closure s ⊆ s ↔ IsClosed s

Dense.inter_of_isOpen_right

theorem Dense.inter_of_isOpen_right : ∀ {X : Type u} {s t : Set X} [inst : TopologicalSpace X], Dense s → Dense t → IsOpen t → Dense (s ∩ t)

Filter.HasBasis.lift'_interior

theorem Filter.HasBasis.lift'_interior : ∀ {X : Type u} {ι : Sort w} [inst : TopologicalSpace X] {l : Filter X} {p : ι → Prop} {s : ι → Set X}, l.HasBasis p s → (l.lift' interior).HasBasis p fun i => interior (s i)

continuous_iff_isClosed

theorem continuous_iff_isClosed : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}, Continuous f ↔ ∀ (s : Set Y), IsClosed s → IsClosed (f ⁻¹' s)

ClusterPt.mono

theorem ClusterPt.mono : ∀ {X : Type u} {x : X} [inst : TopologicalSpace X] {f g : Filter X}, ClusterPt x f → f ≤ g → ClusterPt x g := by sorry

tendsto_nhds

theorem tendsto_nhds : ∀ {X : Type u} {α : Type u_1} {x : X} [inst : TopologicalSpace X] {f : α → X} {l : Filter α}, Filter.Tendsto f l (nhds x) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → f ⁻¹' s ∈ l

mem_interior_iff_mem_nhds

theorem mem_interior_iff_mem_nhds : ∀ {X : Type u} {x : X} {s : Set X} [inst : TopologicalSpace X], x ∈ interior s ↔ s ∈ nhds x

Mathlib.Topology.Basic._auxLemma.62

theorem Mathlib.Topology.Basic._auxLemma.62 : ∀ {X : Type u} {x : X} {s : Set X} [inst : TopologicalSpace X], (x ∈ closure s) = ∀ t ∈ nhds x, (t ∩ s).Nonempty

mem_closure_iff_nhds_basis'

theorem mem_closure_iff_nhds_basis' : ∀ {X : Type u} {ι : Sort w} {x : X} {t : Set X} [inst : TopologicalSpace X] {p : ι → Prop} {s : ι → Set X}, (nhds x).HasBasis p s → (x ∈ closure t ↔ ∀ (i : ι), p i → (s i ∩ t).Nonempty)

closure_compl

theorem closure_compl : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], closure sᶜ = (interior s)ᶜ

Set.Finite.isClosed_biUnion

theorem Set.Finite.isClosed_biUnion : ∀ {X : Type u} {α : Type u_1} [inst : TopologicalSpace X] {s : Set α} {f : α → Set X}, s.Finite → (∀ i ∈ s, IsClosed (f i)) → IsClosed (⋃ i ∈ s, f i)

pure_le_nhds

theorem pure_le_nhds : ∀ {X : Type u} [inst : TopologicalSpace X], pure ≤ nhds

mem_closure_iff_nhds_basis

theorem mem_closure_iff_nhds_basis : ∀ {X : Type u} {ι : Sort w} {x : X} {t : Set X} [inst : TopologicalSpace X] {p : ι → Prop} {s : ι → Set X}, (nhds x).HasBasis p s → (x ∈ closure t ↔ ∀ (i : ι), p i → ∃ y ∈ t, y ∈ s i)

ContinuousAt.preimage_mem_nhds

theorem ContinuousAt.preimage_mem_nhds : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {x : X} {t : Set Y}, ContinuousAt f x → t ∈ nhds (f x) → f ⁻¹' t ∈ nhds x

DenseRange.nonempty_iff

theorem DenseRange.nonempty_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {α : Type u_4} {f : α → X}, DenseRange f → (Nonempty α ↔ Nonempty X)

interior_univ

theorem interior_univ : ∀ {X : Type u} [inst : TopologicalSpace X], interior Set.univ = Set.univ

eventually_nhds_iff

theorem eventually_nhds_iff : ∀ {X : Type u} {x : X} [inst : TopologicalSpace X] {p : X → Prop}, (∀ᶠ (x : X) in nhds x, p x) ↔ ∃ t, (∀ x ∈ t, p x) ∧ IsOpen t ∧ x ∈ t

Disjoint.closure_left

theorem Disjoint.closure_left : ∀ {X : Type u} {s t : Set X} [inst : TopologicalSpace X], Disjoint s t → IsOpen t → Disjoint (closure s) t := by sorry

isOpen_biUnion

theorem isOpen_biUnion : ∀ {X : Type u} {α : Type u_1} [inst : TopologicalSpace X] {s : Set α} {f : α → Set X}, (∀ i ∈ s, IsOpen (f i)) → IsOpen (⋃ i ∈ s, f i)

Dense.inter_nhds_nonempty

theorem Dense.inter_nhds_nonempty : ∀ {X : Type u} {x : X} {s t : Set X} [inst : TopologicalSpace X], Dense s → t ∈ nhds x → (s ∩ t).Nonempty := by sorry

interior_singleton

theorem interior_singleton : ∀ {X : Type u} [inst : TopologicalSpace X] (x : X) [inst_1 : (nhdsWithin x {x}ᶜ).NeBot], interior {x} = ∅ := by sorry

mem_closure_of_tendsto

theorem mem_closure_of_tendsto : ∀ {X : Type u} {α : Type u_1} {x : X} {s : Set X} [inst : TopologicalSpace X] {f : α → X} {b : Filter α} [inst_1 : b.NeBot], Filter.Tendsto f b (nhds x) → (∀ᶠ (x : α) in b, f x ∈ s) → x ∈ closure s

Mathlib.Topology.Basic._auxLemma.1

theorem Mathlib.Topology.Basic._auxLemma.1 : ∀ {X : Type u} [inst : TopologicalSpace X], IsOpen ∅ = True

isClosed_biInter

theorem isClosed_biInter : ∀ {X : Type u} {α : Type u_1} [inst : TopologicalSpace X] {s : Set α} {f : α → Set X}, (∀ i ∈ s, IsClosed (f i)) → IsClosed (⋂ i ∈ s, f i)

DenseRange.subset_closure_image_preimage_of_isOpen

theorem DenseRange.subset_closure_image_preimage_of_isOpen : ∀ {X : Type u_1} [inst : TopologicalSpace X] {α : Type u_4} {f : α → X} {s : Set X}, DenseRange f → IsOpen s → s ⊆ closure (f '' (f ⁻¹' s))

mem_closure_iff_nhds

theorem mem_closure_iff_nhds : ∀ {X : Type u} {x : X} {s : Set X} [inst : TopologicalSpace X], x ∈ closure s ↔ ∀ t ∈ nhds x, (t ∩ s).Nonempty := by sorry

Continuous.tendsto'

theorem Continuous.tendsto' : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}, Continuous f → ∀ (x : X) (y : Y), f x = y → Filter.Tendsto f (nhds x) (nhds y)

interior_subset

theorem interior_subset : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], interior s ⊆ s

all_mem_nhds_filter

theorem all_mem_nhds_filter : ∀ {X : Type u} {α : Type u_1} [inst : TopologicalSpace X] (x : X) (f : Set X → Set α), (∀ (s t : Set X), s ⊆ t → f s ⊆ f t) → ∀ (l : Filter α), (∀ s ∈ nhds x, f s ∈ l) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → f s ∈ l

closure_empty

theorem closure_empty : ∀ {X : Type u} [inst : TopologicalSpace X], closure ∅ = ∅

closure_nonempty_iff

theorem closure_nonempty_iff : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], (closure s).Nonempty ↔ s.Nonempty

Set.Finite.isOpen_sInter

theorem Set.Finite.isOpen_sInter : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set (Set X)}, s.Finite → (∀ t ∈ s, IsOpen t) → IsOpen s.sInter := by sorry

TopologicalSpace.ext

theorem TopologicalSpace.ext : ∀ {X : Type u} {f g : TopologicalSpace X}, IsOpen = IsOpen → f = g

IsClosed.mem_of_frequently_of_tendsto

theorem IsClosed.mem_of_frequently_of_tendsto : ∀ {X : Type u} {α : Type u_1} {x : X} {s : Set X} [inst : TopologicalSpace X] {f : α → X} {b : Filter α}, IsClosed s → (∃ᶠ (x : α) in b, f x ∈ s) → Filter.Tendsto f b (nhds x) → x ∈ s

continuous_const

theorem continuous_const : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {y : Y}, Continuous fun x => y

`nhds_le_of_le`

`isClosed_compl_iff`

`interior_empty`

`continuous_id`

`closure_subset_iff_isClosed`

`Dense.inter_of_isOpen_right`

`Filter.HasBasis.lift'_interior`

`continuous_iff_isClosed`

`ClusterPt.mono`

`tendsto_nhds`

`mem_interior_iff_mem_nhds`

`Mathlib.Topology.Basic._auxLemma.62`

`mem_closure_iff_nhds_basis'`

`closure_compl`

`Set.Finite.isClosed_biUnion`

`pure_le_nhds`

`mem_closure_iff_nhds_basis`

`ContinuousAt.preimage_mem_nhds`

`DenseRange.nonempty_iff`

`interior_univ`

`eventually_nhds_iff`

`Disjoint.closure_left`

`isOpen_biUnion`

`Dense.inter_nhds_nonempty`

`interior_singleton`

`mem_closure_of_tendsto`

`Mathlib.Topology.Basic._auxLemma.1`

`isClosed_biInter`

`DenseRange.subset_closure_image_preimage_of_isOpen`

`mem_closure_iff_nhds`

`Continuous.tendsto'`

`interior_subset`

`all_mem_nhds_filter`

`closure_empty`

`closure_nonempty_iff`

`Set.Finite.isOpen_sInter`

`TopologicalSpace.ext`

`IsClosed.mem_of_frequently_of_tendsto`

`continuous_const`

`frontier_eq_closure_inter_closure`

`accPt_iff_nhds`

`mem_nhds_iff`

`IsOpen.subset_interior_iff`

`mem_closure_iff_ultrafilter`

`Continuous.closure_preimage_subset`

`nhds_basis_opens'`

`closure_eq_compl_interior_compl`

`continuous_iff_ultrafilter`

`isClosed_setOf_clusterPt`

`DenseRange.dense_image`

`mem_of_mem_nhds`

`clusterPt_principal_iff`

`IsClosed.preimage`

`Set.Finite.interior_biInter`

`ContinuousAt.comp`

`interior_inter`

`IsOpen.mem_nhds`

`interior_frontier`

`Set.Nonempty.of_closure`

`IsClosed.closure_subset_iff`

`isOpen_iff_forall_mem_open`

`DenseRange.closure_range`

`Filter.Frequently.mem_closure`

`preimage_interior_subset_interior_preimage`

`Function.Surjective.denseRange`

`interior_compl`

`IsClosed.closure_subset`

`isOpen_iff_eventually`

`Mathlib.Topology.Basic._auxLemma.7`

`interior_maximal`

`closure_mono`

`Filter.EventuallyEq.eq_of_nhds`

`Filter.EventuallyLE.eventuallyLE_nhds`

`exists_open_set_nhds`