eq_of_nhds_eq_nhds
theorem eq_of_nhds_eq_nhds : ∀ {X : Type u} {t t' : TopologicalSpace X}, (∀ (x : X), nhds x = nhds x) → t = t' := by
sorry
This theorem, referred to as `eq_of_nhds_eq_nhds`, establishes that for any type `X`, if two topologies `t` and `t'` on `X` have the property that for every point `x` in `X`, the neighborhood filter of `x` under `t` is the same as the neighborhood filter of `x` under `t'`, then these two topologies `t` and `t'` are in fact the same. In other words, the theorem states that two topologies are equal if and only if the neighborhood filters they generate at each point are identical.
More concisely: Two topologies on a type are equal if and only if they have identical neighborhood filters at each point.
|
induced_id
theorem induced_id : ∀ {α : Type u_1} [t : TopologicalSpace α], TopologicalSpace.induced id t = t
The theorem `induced_id` states that for any type `α` equipped with a topology `t`, the topology induced by the identity function `id` on `α` is the same as the original topology `t`. This means that applying the identity function does not change the topological structure of the space `α`.
More concisely: The identity function preserves the topology on a space, i.e., the topology induced by the identity function on a topological space is equal to the original topology.
|
TopologicalSpace.tendsto_nhds_generateFrom
theorem TopologicalSpace.tendsto_nhds_generateFrom :
∀ {α : Type u} {β : Type u_1} {m : α → β} {f : Filter α} {g : Set (Set β)} {b : β},
(∀ s ∈ g, b ∈ s → m ⁻¹' s ∈ f) → Filter.Tendsto m f (nhds b)
This theorem, named `TopologicalSpace.tendsto_nhds_generateFrom`, asserts the following property about a function's tendency towards a limit within the context of a topological space. Given any types `α` and `β`, a function `m` mapping from `α` to `β`, a filter `f` on `α`, a set `g` of subsets of `β`, and an element `b` of `β`, if for all subsets `s` in `g` such that `b` is in `s`, the preimage of `s` under `m` is in `f`, then `m` tends to the neighborhood filter of `b` (i.e., `Filter.Tendsto m f (nhds b)`). In other words, the function `m` has the property of tending towards a limit `b` (in the filter `f`) if the preimage of any subset of `β` containing `b` is in the filter `f`.
More concisely: If the preimage of every neighborhood of a point under a function is in a given filter, then the function tends to that point with respect to the filter.
|
nhds_nhdsAdjoint_of_ne
theorem nhds_nhdsAdjoint_of_ne : ∀ {α : Type u} {a b : α} (f : Filter α), b ≠ a → nhds b = pure b
This theorem states that for any type `α`, and any two elements `a` and `b` of `α` that are not equal, along with a filter `f` on `α`, the neighborhood filter of `b` is equal to the pure filter of `b`. In other words, the set of all neighborhoods of `b` (each of which is a set that contains an open set around `b`) is equal to the set that contains `b` and nothing else if `b` is not equal to `a`.
More concisely: For any type `α`, filter `f` on `α`, and distinct elements `a` and `b` of `α`, the neighborhood filter of `b` equals the pure point filter of `b` in `f`.
|
DiscreteTopology.eq_bot
theorem DiscreteTopology.eq_bot : ∀ {α : Type u_2} [t : TopologicalSpace α] [self : DiscreteTopology α], t = ⊥ := by
sorry
This theorem states that for any type `α` with a `TopologicalSpace` structure and a `DiscreteTopology` structure, the `TopologicalSpace` structure is equivalent to the bottom element `⊥`. In other words, in the context of a discrete topological space (where all subsets are open), the topology is minimally structured.
More concisely: For any type `α` equipped with both a `TopologicalSpace` and a `DiscreteTopology` structure, the two structures are equivalent, meaning the discrete topology is the finest topology.
|
continuous_coinduced_rng
theorem continuous_coinduced_rng : ∀ {α : Type u} {β : Type v} {f : α → β} {t : TopologicalSpace α}, Continuous f := by
sorry
This theorem states that for any given types `α` and `β`, a function `f` from `α` to `β`, and a topological space `t` on `α`, the function `f` is continuous. In mathematical terms, this theorem is asserting that under the coinduced topology on the range of a function, the function is always continuous.
More concisely: For any types `α`, `β`, and a continuous function `f` from `α` to `β`, the function `f` is continuous with respect to any topology on `α`.
|
forall_open_iff_discrete
theorem forall_open_iff_discrete :
∀ {X : Type u_2} [inst : TopologicalSpace X], (∀ (s : Set X), IsOpen s) ↔ DiscreteTopology X
This theorem, `forall_open_iff_discrete`, states that for any type `X` equipped with a topology (i.e., a topological space), the condition that every subset of `X` is an open set is equivalent to the topology being a discrete topology. In other words, a topological space `X` is a discrete topological space if and only if every subset of `X` is considered open in this topology.
More concisely: A topological space is discrete if and only if every subset is open.
|
Mathlib.Topology.Order._auxLemma.6
theorem Mathlib.Topology.Order._auxLemma.6 :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : DiscreteTopology α] (s : Set α), IsOpen s = True
The theorem `Mathlib.Topology.Order._auxLemma.6` states that for any set `s` of any type `α`, given that `α` has a topological space structure and is equipped with a discrete topology, the set `s` is always open. In other words, in a discrete topological space, all sets are open.
More concisely: In a discrete topological space, every subset is open.
|
induced_compose
theorem induced_compose :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {tγ : TopologicalSpace γ} {f : α → β} {g : β → γ},
TopologicalSpace.induced f (TopologicalSpace.induced g tγ) = TopologicalSpace.induced (g ∘ f) tγ
This theorem states that for any three types `α`, `β`, and `γ`, and a topological space `tγ` on `γ`, and any functions `f : α → β` and `g : β → γ`, the topology induced on `α` by `f` followed by the topology induced by `g` is the same as the topology induced directly by the composition of `g` and `f`. In other words, the process of inducing topologies through composition of functions is associative.
More concisely: For any types `α`, `β`, and `γ`, and topological spaces `tβ` on `β` and `tγ` on `γ`, the topology induced on `α` by the composition `g ∘ f` is equal to the topology induced by first inducing the topology on `β` by `f` and then inducing the topology on `α` by `g`, i.e., `induced_topology tγ (g ∘ f) = induced_topology (induced_topology tβ f) g`.
|
preimage_nhds_coinduced
theorem preimage_nhds_coinduced :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {π : α → β} {s : Set β} {a : α},
s ∈ nhds (π a) → π ⁻¹' s ∈ nhds a
The theorem `preimage_nhds_coinduced` asserts that, for any types `α` and `β` (where `α` has a topological space structure) and any function `π` from `α` to `β`, if a set `s` of type `β` is in the neighborhood of the image of an element `a` (i.e., `s` is close to `π a`), then the preimage of `s` under `π` is in the neighborhood of `a`. In simpler terms, it ensures that if `s` is near to `π a`, then all elements in `α` that map into `s` through `π` are near to `a`.
More concisely: If `π : α → β` is a continuous function, `a ∈ α`, `s ∈ β` is a neighborhood of `π(a)`, then `π⁁⁻¹(s)` is a neighborhood of `a` in `α`.
|
continuous_iff_le_induced
theorem continuous_iff_le_induced :
∀ {α : Type u} {β : Type v} {f : α → β} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace β},
Continuous f ↔ t₁ ≤ TopologicalSpace.induced f t₂
The theorem `continuous_iff_le_induced` states that for any two types `α` and `β`, a function `f` from `α` to `β`, and topologies `t₁` on `α` and `t₂` on `β`, the function `f` is continuous if and only if the topology `t₁` on `α` is coarser than or equal to the topology induced on `α` by mapping `f` from the original topology `t₂` on `β`. In other words, `f` is continuous when every set in the topology of `α` is an open set that is the preimage of an open set in the topology of `β` under the function `f`.
More concisely: A function between two topological spaces is continuous if and only if the topology on the domain is finer than or equal to the topology induced by the function on the codomain.
|
isClosed_induced_iff
theorem isClosed_induced_iff :
∀ {α : Type u_1} {β : Type u_2} [t : TopologicalSpace β] {s : Set α} {f : α → β},
IsClosed s ↔ ∃ t_1, IsClosed t_1 ∧ f ⁻¹' t_1 = s
This theorem states that for any types `α` and `β`, and for any topological space `t` over `β`, a set `s` of type `α` is closed if and only if there exists another set `t_1` such that `t_1` is closed and `t_1` is the preimage of the function `f` from `α` to `β` applied to `s`. In other words, `s` is closed under the topology induced by `f` if there is a closed set in `β` that `f` maps `s` onto.
More concisely: A set in type `α` is closed with respect to a topology `t` over `β` if and only if it is the preimage under `f` of some closed set in `β`.
|
nhds_iInf
theorem nhds_iInf : ∀ {α : Type u} {ι : Sort u_1} {t : ι → TopologicalSpace α} {a : α}, nhds a = ⨅ i, nhds a
The theorem `nhds_iInf` asserts that for any type `α`, any index type `ι`, any function `t` that maps from index type `ι` to `TopologicalSpace α`, and any element `a` of type `α`, the neighborhood filter `nhds a` is equal to the infimum of the neighborhood filters `nhds a` over all `i` in index type `ι`. This means that the neighborhood of a point `a` in a topological space is the smallest filter that contains all the neighborhood filters of `a` for each topology created by the function `t`.
More concisely: The neighborhood filter of a point in a topological space is the infimum of the neighborhood filters of that point under all possible topologies on the space.
|
induced_const
theorem induced_const :
∀ {α : Type u_1} {β : Type u_2} [t : TopologicalSpace α] {x : α}, TopologicalSpace.induced (fun x_1 => x) t = ⊤
The theorem `induced_const` states that for any types `α` and `β`, given a topological space `t` on `α` and any element `x` of `α`, the topology on `β` induced by the constant function mapping each element to `x` is the discrete topology (denoted by `⊤`). In other words, every subset of `β` is an open set in the induced topology. This is because the preimage of any set through a constant function is either the whole space (if the set contains the constant value) or the empty set (if it doesn't), both of which are always open in any topology.
More concisely: For any topological spaces `t` on types `α` and `β`, and any element `x` of `α`, the topology on `β` induced by the constant function mapping every element to `x` is the discrete topology.
|
nhds_mono
theorem nhds_mono : ∀ {α : Type u} {t₁ t₂ : TopologicalSpace α} {a : α}, t₁ ≤ t₂ → nhds a ≤ nhds a
The theorem `nhds_mono` asserts that for any type `α` and any two topological spaces `t₁` and `t₂` over `α`, and any element `a` of `α`, if `t₁` is a subtopology of `t₂` (i.e., `t₁ ≤ t₂`), then the neighborhood filter of `a` in `t₁` is a subfilter of the neighborhood filter of `a` in `t₂`. In other words, every neighborhood of `a` in the smaller topology is also a neighborhood of `a` in the larger topology.
More concisely: For any type `α`, if `t₁` is a subtopology of `t₂` over `α` and `a` is an element of `α`, then the neighborhood filter of `a` in `t₁` is contained in the neighborhood filter of `a` in `t₂`.
|
gc_coinduced_induced
theorem gc_coinduced_induced :
∀ {α : Type u_1} {β : Type u_2} (f : α → β),
GaloisConnection (TopologicalSpace.coinduced f) (TopologicalSpace.induced f)
This theorem states that for all types `α` and `β` and a function `f` from `α` to `β`, there exists a Galois connection between the coinduced topology on `β` (which is the finest topology that makes `f` continuous) and the induced topology on `α` (which is the coarsest topology that makes `f` continuous). In other words, a subset `s` of `β` is open in the coinduced topology if and only if its preimage under `f` is open in the induced topology on `α`. This Galois connection provides a relation between the two topologies induced by the function `f`.
More concisely: For every function `f` from type `α` to type `β`, the coinduced topology on `β` and the induced topology on `α` form a Galois connection, where a subset `s` of `β` is open in the coinduced topology if and only if `f⁁¹(s)` is open in the induced topology on `α`.
|
continuous_id_of_le
theorem continuous_id_of_le : ∀ {α : Type u} {t t' : TopologicalSpace α}, t ≤ t' → Continuous id
This theorem states that if you have any type `α` and two topological spaces `t` and `t'` over `α`, with `t` being a subset of `t'` (that is, `t` is finer than or equal to `t'`), then the identity function is continuous. In mathematical terms, if a topology `t` is less than or equal to a topology `t'` on a given set `α`, the identity function from `α` to `α` is a continuous function with respect to these topologies.
More concisely: If `α` is a type and `t` is a topology on `α` that is finer than or equal to topology `t'` on `α`, then the identity function `id : α → α` is continuous from `(α, t)` to `(α, t')`.
|
continuous_bot
theorem continuous_bot : ∀ {α : Type u} {β : Type v} {f : α → β} {t : TopologicalSpace β}, Continuous f
This theorem states that for any two types `α` and `β`, and for any function `f` from `α` to `β`, and for any topology `t` on `β`, the function `f` is continuous. In mathematical terms, this corresponds to the definition that a function is continuous if the preimage of every open set is open, for all types and all functions between them, regardless of the topology on the codomain.
More concisely: For any types `α` and `β`, and any function `f` from `α` to `β`, if `t` is a topology on `β`, then `f` is continuous with respect to `t` if and only if the preimage of every open set in `β` under `f` is open in `α`.
|
induced_inf
theorem induced_inf :
∀ {α : Type u_1} {β : Type u_2} {t₁ t₂ : TopologicalSpace α} {g : β → α},
TopologicalSpace.induced g (t₁ ⊓ t₂) = TopologicalSpace.induced g t₁ ⊓ TopologicalSpace.induced g t₂
The theorem `induced_inf` states that for any two topological spaces `t₁` and `t₂` over a type `α`, and for any function `g` from a type `β` to `α`, the topology induced on `β` by the intersection of `t₁` and `t₂` (denoted `t₁ ⊓ t₂`) under the function `g` is the same as the intersection of the topologies induced by `t₁` and `t₂` separately under the same function `g`. In other words, the order of intersection and topology induction does not matter.
More concisely: For topological spaces $t\_1$, $t\_2$ over type $\alpha$ and a function $g:\beta\to\alpha$, the topology induced by $t\_1 \cap t\_2$ on $\beta$ via $g$ equals the intersection of the topologies induced by $t\_1$ and $t\_2$ on $\beta$ via $g$.
|
continuous_le_dom
theorem continuous_le_dom :
∀ {α : Type u} {β : Type v} {f : α → β} {t₁ t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β},
t₂ ≤ t₁ → Continuous f → Continuous f
This theorem, `continuous_le_dom`, states that for any two topological spaces `t₁` and `t₂` over a set of type `α` and a function `f` from `α` to another set of type `β` in a topological space `t₃`, if the topology `t₂` is a subset of or equal to the topology `t₁`, then the continuity of `f` with respect to `t₁` and `t₃` implies its continuity with respect to `t₂` and `t₃`. In other words, if a function is continuous in a coarser (larger) topology, it continues to be continuous in a finer (smaller or equal) topology.
More concisely: If `f` is continuous from `(α, t₁)` to `(β, t₃)` and `t₂ ⊆ t₁`, then `f` is continuous from `(α, t₂)` to `(β, t₃)`.
|
TopologicalSpace.gc_generateFrom
theorem TopologicalSpace.gc_generateFrom :
∀ (α : Type u_1),
GaloisConnection (fun t => OrderDual.toDual {s | IsOpen s}) (TopologicalSpace.generateFrom ∘ ⇑OrderDual.ofDual)
The theorem `TopologicalSpace.gc_generateFrom` asserts that for any type `α`, there exists a Galois connection between the function that maps a set to the dual order of the set of its open subsets and the generator function of the smallest topological space containing a collection of basic sets transformed by the dual order of a linear order function. In other words, the theorem describes a relationship between certain operations on open sets in topological spaces and the generation of topological spaces from sets of basic open sets under an order reversal. Thus, it creates a link between the structure of topological spaces and the dual order of their open sets.
More concisely: The theorem `TopologicalSpace.gc_generateFrom` states that for any type `α`, there exists a Galois connection between the function mapping sets to their dual orders of open subsets and the generator function of the smallest topological space containing a collection of basic sets transformed by a linear order's dual order.
|
nhds_sInf
theorem nhds_sInf : ∀ {α : Type u} {s : Set (TopologicalSpace α)} {a : α}, nhds a = ⨅ t ∈ s, nhds a
This theorem, denoted as `nhds_sInf`, states that for any type `α`, any set `s` of topological spaces on `α`, and any element `a` of type `α`, the neighborhood filter at `a` is equal to the infimum of the neighborhood filters at `a` for all topological spaces in `s`. In mathematical terms, the neighborhood filter at any point `a` in a given topological space is the same as the greatest lower bound (infimum) of the neighborhood filters at point `a` across all topological spaces within a specified set.
More concisely: For any type `α`, any set `s` of topological spaces on `α`, and any `a` in `α`, the neighborhood filter of `a` is the infimum of the neighborhood filters of `a` in all topologies in `s`.
|
continuous_iff_coinduced_le
theorem continuous_iff_coinduced_le :
∀ {α : Type u} {β : Type v} {f : α → β} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace β},
Continuous f ↔ TopologicalSpace.coinduced f t₁ ≤ t₂
This theorem states that for any two types `α` and `β`, a function `f` from `α` to `β`, and topological spaces `t₁` on `α` and `t₂` on `β`, the function `f` is continuous if and only if the coinduced topology on `β` from `f` and `t₁` is less than or equal to `t₂`. In other words, a function is continuous if the finest topology (coinduced topology) on the codomain that makes the function continuous is a subtopology of the given topology on the codomain.
More concisely: A function between two topological spaces is continuous if and only if the coinduced topology on its codomain is a subtopology of the given topology on the codomain.
|
TopologicalSpace.generateFrom_anti
theorem TopologicalSpace.generateFrom_anti :
∀ {α : Type u_1} {g₁ g₂ : Set (Set α)},
g₁ ⊆ g₂ → TopologicalSpace.generateFrom g₂ ≤ TopologicalSpace.generateFrom g₁
This theorem states that for any type `α` and any two collections of sets `g₁` and `g₂` of `α`, if `g₁` is a subset of `g₂`, then the smallest topological space containing `g₂` is a smaller (or equal) topological space than the smallest topological space containing `g₁`. In other words, adding more basic sets to generate a topological space can only result in a larger (or equal) topological space.
More concisely: For any type `α` and any collections `g₁` and `g₂` of subsets of `α` with `g₁` being a subset of `g₂`, the smallest topological space containing `g₂` is no larger than the smallest topological space containing `g₁`.
|
TopologicalSpace.le_generateFrom_iff_subset_isOpen
theorem TopologicalSpace.le_generateFrom_iff_subset_isOpen :
∀ {α : Type u} {g : Set (Set α)} {t : TopologicalSpace α},
t ≤ TopologicalSpace.generateFrom g ↔ g ⊆ {s | IsOpen s}
This theorem states that for any type `α`, any set `g` of sets of `α`, and any topological space `t` defined on `α`, the topological space `t` is less than or equal to the topological space generated by `g` if and only if `g` is a subset of the set of all sets `s` such that `s` is open in the topological space `t`. In other words, a given topological space is smaller than or equal to the space generated by a collection of sets if and only if all the sets in the collection are open in the original space.
More concisely: A topological space is equal to or smaller than the topological space generated by a set of opens if and only if that set of opens is a subset of the opens in the original space.
|
isOpen_discrete
theorem isOpen_discrete :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : DiscreteTopology α] (s : Set α), IsOpen s
The theorem `isOpen_discrete` states that for any type `α` that has a topological space structure and a discrete topology structure, any set `s` of type `α` is open in this topological space. In other words, in a discrete topological space, every set is an open set.
More concisely: In a discrete topological space, every subset is open.
|
TopologicalSpace.isOpen_top_iff
theorem TopologicalSpace.isOpen_top_iff : ∀ {α : Type u_2} (U : Set α), IsOpen U ↔ U = ∅ ∨ U = Set.univ
This theorem states that for any type `α` and a set `U` of `α`, the set `U` is open in the indiscrete topology if and only if `U` is either the empty set or the whole space. In other words, in the indiscrete topology, the only open sets are the empty set and the entire space.
More concisely: In the indiscrete topology, a set is open if and only if it is either the empty set or the entire space.
|
TopologicalSpace.nhds_mkOfNhds_of_hasBasis
theorem TopologicalSpace.nhds_mkOfNhds_of_hasBasis :
∀ {α : Type u} {n : α → Filter α} {ι : α → Sort u_1} {p : (a : α) → ι a → Prop} {s : (a : α) → ι a → Set α},
(∀ (a : α), (n a).HasBasis (p a) (s a)) →
(∀ (a : α) (i : ι a), p a i → a ∈ s a i) →
(∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x) → ∀ (a : α), nhds a = n a
The theorem `TopologicalSpace.nhds_mkOfNhds_of_hasBasis` states that for any type `α`, a mapping `n` from `α` to a filter on `α`, a dependent type `ι` indexed by `α`, a predicate `p` and a mapping `s` from `α` and `ι a` to a set of `α`, given that:
1. For every `a` in `α`, `n a` has a basis given by the predicate `p a` and the set function `s a`.
2. For every `a` in `α` and `i` in `ι a`, if the predicate `p a i` is true, then `a` belongs to the set `s a i`.
3. For every `a` in `α` and `i` in `ι a`, if the predicate `p a i` is true, then for every element `x` in `α` that eventually belongs to `n a`, `s a i` belongs to `n x`.
Then the neighborhood filter at `a`, denoted `nhds a`, is equal to `n a`. This theorem characterizes the neighborhood filter in terms of a filter and its basis, and provides conditions under which they are equal.
More concisely: Given a filter `n` on a type `α`, a basis for `n` at each point `α` given by a predicate `p` and a set function `s`, if for all `a` in `α` and `i` in `ι a` such that `p a i` holds, `a` is in `s a i` and `s a i` is a neighborhood of `x` in `n x`, then `nhds a = n a`.
|
continuous_generateFrom
theorem continuous_generateFrom :
∀ {α : Type u} {β : Type v} {f : α → β} {t : TopologicalSpace α} {b : Set (Set β)},
(∀ s ∈ b, IsOpen (f ⁻¹' s)) → Continuous f
This theorem, referred to as an alias of the reverse direction of `continuous_generateFrom_iff`, states that for any types `α` and `β`, function `f` from `α` to `β`, topological space `t` on `α`, and set `b` of subsets of `β`, if the preimage of every set `s` in `b` under the function `f` is open (in the sense of the topological space), then the function `f` is continuous. In other words, if for each set in `b`, its preimage through the function `f` yields an open set, then `f` is a continuous function.
More concisely: If the preimages under a function between topological spaces are open for all sets in a given collection, then the function is continuous.
|
TopologicalSpace.nhds_generateFrom
theorem TopologicalSpace.nhds_generateFrom :
∀ {α : Type u} {g : Set (Set α)} {a : α}, nhds a = ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, Filter.principal s
The theorem `TopologicalSpace.nhds_generateFrom` states that for any type `α`, any set `g` of subsets of `α`, and any element `a` of `α`, the neighborhood filter at `a` is equal to the infimum (greatest lower bound) of the principal filters of all sets `s` such that `a` is in `s` and `s` is in `g`. In other words, the neighborhood of a point in a space is generated from the collection of all supersets of sets that both contain the point and are elements of a given set of sets.
More concisely: The neighborhood filter of a point in a topological space is the infimum of the principal filters of all sets containing the point that belong to a given set of subsets of the space.
|
Continuous.le_induced
theorem Continuous.le_induced :
∀ {α : Type u_1} {β : Type u_2} {t : TopologicalSpace α} {t' : TopologicalSpace β} {f : α → β},
Continuous f → t ≤ TopologicalSpace.induced f t'
This theorem states that for any two types `α` and `β`, and any topological spaces `t` on `α` and `t'` on `β`, if a function `f : α → β` is continuous, then the topology `t` is finer than or equal to the topology induced by `f` on `α` with respect to the topology `t'` on `β`. In other words, any open set in `t` is also an open set in the induced topology. Here, the term "finer than" in terms of topologies signifies that a topology has more open sets.
More concisely: Given types `α` and `β`, topologies `t` on `α` and `t'` on `β`, and a continuous function `f : α → β`, the topology `t` is included in the topology `t'` induced on `α` by `f`.
|
gc_nhds
theorem gc_nhds : ∀ {α : Type u} (a : α), GaloisConnection (nhdsAdjoint a) fun t => nhds a
The theorem `gc_nhds` states that for any type `α` and any element `a` of that type, there exists a Galois connection between the function `nhdsAdjoint a` and the function `t => nhds a`. In other words, for every `a` in `α`, the function which assigns a topological space to each filter on `α` using `nhdsAdjoint a`, and the function which sends each topological space to the neighborhood filter at `a`, satisfy the properties of a Galois connection. In terms of order theory, this means that for all filters and topological spaces in their respective orders, the value of `nhdsAdjoint a` on a filter is less than or equal to a topological space if and only if the filter is less than or equal to the value of `nhds a` on the topological space.
More concisely: For every type `α` and element `a` in `α`, the functions `nhdsAdjoint a` and `nhds a` form a Galois connection between filters on `α` and topological spaces over `α`.
|
induced_iInf
theorem induced_iInf :
∀ {α : Type u_1} {β : Type u_2} {g : β → α} {ι : Sort w} {t : ι → TopologicalSpace α},
TopologicalSpace.induced g (⨅ i, t i) = ⨅ i, TopologicalSpace.induced g (t i)
This theorem states that for all types `α` and `β`, a function `g` from `β` to `α`, an index type `ι`, and a function `t` mapping each element of `ι` to a TopologicalSpace on `α`, the topology on `β` induced by the function `g` and the infimum (greatest lower bound) of the topologies `t i` (for all `i` in `ι`) is equal to the infimum of the topologies on `β` induced by the same function `g` and each of the topologies `t i`. In other words, the process of inducing a topology commutes with taking the infimum of a collection of topologies. In mathematical terms, it's saying that if $g: \beta \rightarrow \alpha$ and $\text{t} : \iota \rightarrow \text{TopologicalSpace} \ \alpha$, then $\text{TopologicalSpace.induced} \ g \ (\bigwedge_i \text{t} \ i) = \bigwedge_i \ \text{TopologicalSpace.induced} \ g \ (\text{t} \ i)$.
More concisely: For all types `α`, `β`, index type `ι`, functions `g : β -> α` and `t : ι -> TopologicalSpace α`, the topology on `β` induced by `g` from the infimum of `t i` (for all `i` in `ι`) is equal to the infimum of the topologies on `β` induced by `g` and each `t i`. In other words, `TopologicalSpace.induced g (⨄ i in ι . t i) = ⨄ i in ι . TopologicalSpace.induced g (t i)`.
|
continuous_induced_rng
theorem continuous_induced_rng :
∀ {α : Type u} {β : Type v} {γ : Type u_1} {f : α → β} {g : γ → α} {t₂ : TopologicalSpace β}
{t₁ : TopologicalSpace γ}, Continuous g ↔ Continuous (f ∘ g)
This theorem states that for any three types `α`, `β`, and `γ`, and for any two functions `f` from `α` to `β` and `g` from `γ` to `α`, given the topological spaces `t₂` on `β` and `t₁` on `γ`, the function `g` is continuous if and only if the composition of `f` and `g` is continuous. In other words, the continuity of the function `g` can be deduced from the continuity of the composite function `f ∘ g`.
More concisely: For any types `α`, `β`, and `γ`, and functions `f : α → β` and `g : γ → α`, the function `g` is continuous if and only if the composition `f ∘ g` is continuous with respect to the given topologies on `β` and `γ`.
|
isClosed_induced_iff'
theorem isClosed_induced_iff' :
∀ {α : Type u_1} {β : Type u_2} [t : TopologicalSpace β] {f : α → β} {s : Set α},
IsClosed s ↔ ∀ (a : α), f a ∈ closure (f '' s) → a ∈ s
This theorem states that for any two types `α` and `β`, a topological space `t` over `β`, a function `f` from `α` to `β`, and a set `s` of `α`, the set `s` is closed if and only if for every element `a` of `α`, if `f(a)` is in the closure of the image of `s` under `f`, then `a` must belong to `s`. In other words, the closure of the image of `s` under `f` is such that any `a` in `α` that maps into this closure must have come from `s`. This theorem provides a characterization of closed sets in terms of their images under a function in the context of topological spaces.
More concisely: A set in a topological space is closed if and only if the closure of its image under any continuous function contains only elements mapping from the set itself.
|
isOpen_induced_iff
theorem isOpen_induced_iff :
∀ {α : Type u_1} {β : Type u_2} [t : TopologicalSpace β] {s : Set α} {f : α → β},
IsOpen s ↔ ∃ t_1, IsOpen t_1 ∧ f ⁻¹' t_1 = s
The theorem `isOpen_induced_iff` states that for any types `α` and `β`, a topological space `t` on `β`, a set `s` of type `α`, and a function `f` from `α` to `β`, the set `s` is open if and only if there exists a set `t_1` such that `t_1` is open and the preimage of `t_1` under the function `f` is equal to `s`. This characterizes an open set in the induced topology, where the open sets are the preimages of open sets in the original space.
More concisely: A set in the induced topology is open if and only if it is the preimage of some open set under a continuous function.
|
continuous_id_iff_le
theorem continuous_id_iff_le : ∀ {α : Type u} {t t' : TopologicalSpace α}, Continuous id ↔ t ≤ t'
This theorem states that for all types `α` and for any two topological spaces `t` and `t'` over `α`, the identity function is continuous if and only if the topological space `t` is a subspace of the topological space `t'`. In other words, it says that the continuity of the identity function is equivalent to the ordering of the two topological spaces.
More concisely: The identity function is continuous from a topological space (t) to another (t') if and only if t is a subspace of t'.
|
nhds_discrete
theorem nhds_discrete : ∀ (α : Type u_3) [inst : TopologicalSpace α] [inst_1 : DiscreteTopology α], nhds = pure := by
sorry
The theorem `nhds_discrete` states that for any type `α` with a topological space structure and a discrete topology, the neighborhood filter at any point is equal to the singleton set containing that point. In other words, in a discrete topological space, a neighborhood of a point `x` is just the set `{x}` itself. This is because, in a discrete topology, every single set, including singletons, is open.
More concisely: In a discrete topological space, the neighborhood filter of a point is equal to the singleton set containing that point.
|
singletons_open_iff_discrete
theorem singletons_open_iff_discrete :
∀ {X : Type u_2} [inst : TopologicalSpace X], (∀ (a : X), IsOpen {a}) ↔ DiscreteTopology X
This theorem states that for every type `X` equipped with a certain topological space structure, the condition that every singleton set `{a}` is open in this topological space is equivalent to the topology being a discrete topology. In other words, in any topological space, if every single-element set is an open set, then that topology is a discrete topology, and vice versa.
More concisely: In a topological space, the topology is discrete if and only if every singleton set is open.
|
continuous_of_discreteTopology
theorem continuous_of_discreteTopology :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : DiscreteTopology α] {β : Type u_2}
[inst_2 : TopologicalSpace β] {f : α → β}, Continuous f
This theorem states that for any two types `α` and `β` where `α` is equipped with a topological space structure and a discrete topology, and `β` is equipped with a topological space structure, any function `f` from `α` to `β` is continuous. Essentially, this means if we have a space with a discrete topology, any function mapping from this space to another topological space is guaranteed to be continuous.
More concisely: For any types `α` and `β` with discrete topologies, and any function `f : α → β`, `f` is continuous.
|
le_of_nhds_le_nhds
theorem le_of_nhds_le_nhds : ∀ {α : Type u_1} {t₁ t₂ : TopologicalSpace α}, (∀ (x : α), nhds x ≤ nhds x) → t₁ ≤ t₂ := by
sorry
This theorem states that for any type 'α', and any two topological spaces 't₁' and 't₂' over 'α', if for all elements 'x' of type 'α', the neighborhood of 'x' in 't₁' is a subset of the neighborhood of 'x' in 't₂', then 't₁' is a subset of 't₂'. In mathematical terms, if for every 'x' in 'α', every neighborhood of 'x' in space 't₁' is also a neighborhood in space 't₂', then 't₁' is subsumed by (or is smaller than or equal to) 't₂' in the lattice of topological spaces on 'α'. The neighborhood of a point 'x' is a set that contains an open set around 'x'.
More concisely: If for all x in α, the neighborhood filter of x in t₁ is contained in the neighborhood filter of x in t₂, then t₁ is a subspace of t₂.
|
le_generateFrom
theorem le_generateFrom :
∀ {α : Type u} {t : TopologicalSpace α} {g : Set (Set α)},
(∀ s ∈ g, IsOpen s) → t ≤ TopologicalSpace.generateFrom g
This theorem states that for any type `α`, given a topological space `t` over this type and a set `g` of subsets of `α`, if every set in `g` is open in the topological space `t`, then `t` is coarser (i.e., less fine or equal) than the topological space generated from `g`. This generated topology consists of the smallest topological space that contains `g` as their open sets.
In mathematical terms, we have a topological space `(α, t)` and a collection `g` of its open subsets. If `g` contains only open sets of `(α, t)`, then the topology `t` is less fine than or equal to the topology generated from the sets in `g`.
More concisely: If a collection `g` of subsets of a topological space `(α, t)` consists only of open sets, then the topology generated from `g` is coarser than or equal to `t`.
|
DiscreteTopology.of_continuous_injective
theorem DiscreteTopology.of_continuous_injective :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
[inst_2 : DiscreteTopology β] {f : α → β}, Continuous f → Function.Injective f → DiscreteTopology α
This theorem states that if there is a continuous injective function whose codomain has a discrete topology, then its domain also has a discrete topology. In other words, if a function maps distinct elements from its domain to distinct elements in its codomain, and if the codomain is such that every subset is open (which is the defining characteristic of a discrete topology), then every subset of the domain is also open, making the domain a discrete topological space as well. This theorem is applicable in the field of topology, which is a branch of mathematics concerned with the properties of space that are preserved under continuous transformations.
More concisely: If a continuous injective function maps between topological spaces and its codomain has a discrete topology, then its domain also has a discrete topology.
|
continuous_coinduced_dom
theorem continuous_coinduced_dom :
∀ {α : Type u} {β : Type v} {γ : Type u_1} {f : α → β} {g : β → γ} {t₁ : TopologicalSpace α}
{t₂ : TopologicalSpace γ}, Continuous g ↔ Continuous (g ∘ f)
The theorem `continuous_coinduced_dom` states that for any types `α`, `β`, and `γ`, and any functions `f` from `α` to `β` and `g` from `β` to `γ`, given a topological space over `α` and another over `γ`, the function `g` is continuous if and only if the composition of `g` and `f` (`g ∘ f`) is continuous. This is a statement about the preservation of continuity under function composition in the context of topological spaces.
More concisely: Given functions `f: α → β` and `g: β → γ` between topological spaces, `g` is continuous if and only if the composition `g ∘ f` is continuous.
|
nhds_induced
theorem nhds_induced :
∀ {α : Type u} {β : Type v} [T : TopologicalSpace α] (f : β → α) (a : β), nhds a = Filter.comap f (nhds (f a)) := by
sorry
The theorem `nhds_induced` states that for any types `α` and `β`, given a topological space `T` on `α`, a function `f` from `β` to `α`, and an element `a` of `β`, the neighborhood filter of `a` is equal to the preimage (under the function `f`) of the neighborhood filter of `f(a)`. In other words, the local properties around `a` in the space `β` (as described by the neighborhood filter) are exactly those that come from the local properties around `f(a)` in the space `α`, as described by the neighborhood filter of `f(a)`, mapped back via the function `f`.
More concisely: For any topological spaces T on α and β, function f from β to α, and element a of β, the neighborhood filter of a in β is equal to the preimage under f of the neighborhood filter of f(a) in α.
|
coinduced_le_iff_le_induced
theorem coinduced_le_iff_le_induced :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {tα : TopologicalSpace α} {tβ : TopologicalSpace β},
TopologicalSpace.coinduced f tα ≤ tβ ↔ tα ≤ TopologicalSpace.induced f tβ
This theorem states that for any two types `α` and `β`, and any function `f : α → β` between them, and given any topologies `tα` on `α` and `tβ` on `β`, the coinduced topology on `β` from `α` via `f` is less than or equal to `tβ` if and only if `tα` is less than or equal to the topology on `α` induced from `β` via `f`. In other words, it provides a relationship between the coinduced topology and the induced topology through a function between two topological spaces.
More concisely: For any functions `f : α → β` between topological spaces `(α, tα)` and `(β, tβ)`, the coinduced topology on `β` is less than or equal to `tβ` if and only if the induced topology on `α` is less than or equal to `tα`.
|
TopologicalSpace.isOpen_generateFrom_of_mem
theorem TopologicalSpace.isOpen_generateFrom_of_mem : ∀ {α : Type u} {g : Set (Set α)} {s : Set α}, s ∈ g → IsOpen s
The theorem `TopologicalSpace.isOpen_generateFrom_of_mem` declares that for any type `α`, any collection of sets `g` of type `Set α`, and any set `s` of type `Set α`, if `s` belongs to `g`, then `s` is an open set in the topological space generated by `g`. The term "open set" here is used in the context of topology, where an open set is a set that, intuitively, does not include its boundary.
More concisely: In the topology generated by a collection of sets `g` of type `Set α`, any set `s` that belongs to `g` is an open set.
|
induced_generateFrom_eq
theorem induced_generateFrom_eq :
∀ {α : Type u_1} {β : Type u_2} {b : Set (Set β)} {f : α → β},
TopologicalSpace.induced f (TopologicalSpace.generateFrom b) =
TopologicalSpace.generateFrom (Set.preimage f '' b)
This theorem states that for any types `α` and `β`, a set `b` of sets of `β`, and a function `f` from `α` to `β`, the topology induced on `α` by the function `f` and the topology generated from `b` on `β` is equal to the topology on `α` generated by the preimage under `f` of each set in `b`. In simpler terms, we can generate a topology on `α` by taking the preimages of a collection of sets under a function, and this topology is the same as the one we would get by first generating a topology on `β` from the collection and then inducing a topology on `α` through the function.
More concisely: The topology on a type `α` induced by a function `f` from `α` to `β` and a collection `b` of sets of `β`, is equal to the topology on `α` generated by the preimages under `f` of sets in `b`.
|
coinduced_compose
theorem coinduced_compose :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [tα : TopologicalSpace α] {f : α → β} {g : β → γ},
TopologicalSpace.coinduced g (TopologicalSpace.coinduced f tα) = TopologicalSpace.coinduced (g ∘ f) tα
The theorem named `coinduced_compose` states that for any three types `α`, `β`, and `γ`, given a topological space on `α`, and two functions `f` from `α` to `β` and `g` from `β` to `γ`, the coinduced topology on `γ` by `g` from the coinduced topology on `β` by `f` from the topological space on `α` is equivalent to the coinduced topology on `γ` by the composition of `g` and `f` from the topological space on `α`. In other words, the process of coinducing topologies is compatible with function composition.
More concisely: The coinduced topologies on `γ` by the composition of `g` and `f` from the topological space on `α` is equivalent to the coinduced topology on `γ` by `g` from the coinduced topology on `β` by `f` from the topological space on `α`.
|
Mathlib.Topology.Order._auxLemma.31
theorem Mathlib.Topology.Order._auxLemma.31 : ∀ {α : Type u} {a : α} {p : α → Prop}, (a ∈ {x | p x}) = p a
This theorem states that for any types `α` and `β`, and any function `f` from `α` to `β`, also any given topological spaces `t₁` on `α` and `t₂` on `β`, the function `f` is continuous if and only if the coinduced topology on `β` from `f` and `t₁` is a subset of `t₂`. In layman's terms, this theorem is elaborating a condition for a function to be continuous between two topological spaces: it states that a function is continuous if the finest topology on the codomain, which makes the function continuous, is less than or equal to the original topology on the codomain.
More concisely: A function between two topological spaces is continuous if and only if the coinduced topology on the codomain is a subset of the given topology on the codomain.
|
continuous_sInf_dom
theorem continuous_sInf_dom :
∀ {α : Type u} {β : Type v} {f : α → β} {t₁ : Set (TopologicalSpace α)} {t₂ : TopologicalSpace β}
{t : TopologicalSpace α}, t ∈ t₁ → Continuous f → Continuous f
This theorem states that given any types `α` and `β`, a function `f` from `α` to `β`, a set `t₁` of topological spaces over `α`, a topological space `t₂` over `β`, and a topological space `t` over `α`, if `t` is an element of `t₁`, and if the function `f` is continuous, then the function `f` is still continuous. Essentially, the theorem asserts the continuity of a function `f` does not change regardless of whether the topological space in the domain is in a set of such spaces or not.
More concisely: Given types `α`, `β`, a function `f` from `α` to `β`, a topological space `t` over `α`, and a set `t₁` of topological spaces over `α`, if `t` is an element of `t₁` and `f` is continuous, then `f` is continuous with respect to `t₂`, the topological space over `β`.
|
continuous_induced_dom
theorem continuous_induced_dom : ∀ {α : Type u} {β : Type v} {f : α → β} {t : TopologicalSpace β}, Continuous f := by
sorry
This theorem states that for any two types `α` and `β`, and any function `f` from `α` to `β`, and any topological space `t` defined over `β`, the function `f` is continuous. In other words, in the context of topology, this theorem is asserting that under these conditions, the image of an open set under the function `f` will always be an open set in `β`.
More concisely: Given any function `f` from type `α` to type `β` and any topology `t` on `β`, `f` is continuous if for every open set `U ∈ t`, the preimage `f⁻¹(U)` is an open set in `α`.
|
continuous_sInf_rng
theorem continuous_sInf_rng :
∀ {α : Type u} {β : Type v} {f : α → β} {t₁ : TopologicalSpace α} {T : Set (TopologicalSpace β)},
Continuous f ↔ ∀ t ∈ T, Continuous f
This theorem, `continuous_sInf_rng`, states that for any two types `α` and `β`, a function `f` mapping `α` to `β`, a topological space `t₁` on `α`, and a set `T` of topological spaces on `β`, the function `f` is continuous if and only if `f` is continuous for every topological space in the set `T`. In other words, the continuity of a function across different topological spaces is dependent on its continuity in each individual space within the set of all such spaces.
More concisely: A function between two types is continuous with respect to all topologies in a given set if and only if it is continuous under each of those topologies.
|
IsClosed.mono
theorem IsClosed.mono : ∀ {α : Type u_1} {t₁ t₂ : TopologicalSpace α} {s : Set α}, IsClosed s → t₁ ≤ t₂ → IsClosed s
The theorem `IsClosed.mono` states that for any types `α` and any two topological spaces `t₁` and `t₂` on `α`, if a set `s` of type `α` is closed in the first topological space `t₁`, and the first topological space `t₁` is a subset of or equal to the second topological space `t₂` (ie., `t₁ ≤ t₂`), then set `s` is also closed in the second topological space `t₂`. This theorem is asserting the preservation of the closure of a set under the subset or equality relation between topological spaces.
More concisely: If a set is closed in a topological space that is a subset or equal to another topological space, then the set is closed in the larger topological space.
|
isOpen_coinduced
theorem isOpen_coinduced :
∀ {α : Type u_1} {β : Type u_2} {t : TopologicalSpace α} {s : Set β} {f : α → β}, IsOpen s ↔ IsOpen (f ⁻¹' s) := by
sorry
The theorem `isOpen_coinduced` states that for any types `α` and `β`, a given topological space `t` on `α`, a set `s` of elements of type `β`, and a function `f` from `α` to `β`, the set `s` is open if and only if the preimage of `s` under `f` is open. In other words, a set in the codomain of a function is open in the topology induced by that function if and only if its preimage is open in the original topology.
More concisely: For any topological spaces `α` and `β`, function `f` from `α` to `β`, and sets `s` in `β`, the preimage `f⁻¹[s]` is open in `α` if and only if `s` is open in the coinduced topology on `β` by `f`.
|
isOpen_iSup_iff
theorem isOpen_iSup_iff :
∀ {α : Type u} {ι : Sort v} {t : ι → TopologicalSpace α} {s : Set α}, IsOpen s ↔ ∀ (i : ι), IsOpen s
This theorem states that for any type `α`, sort `ι`, a function `t` from `ι` to `TopologicalSpace α`, and a set `s` of type `α`, the set `s` is open if and only if for every element `i` of sort `ι`, `s` is open. In other words, this theorem characterizes an open set in a topological space, stating that a set `s` is open if all instances of `s` (as defined by the elements from `ι`) are also open in their respective topological space.
More concisely: A set in a topological space is open if and only if the image of every element in the indexing type under the given function is an open set in its respective topological space.
|
isClosed_discrete
theorem isClosed_discrete :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : DiscreteTopology α] (s : Set α), IsClosed s
This theorem states that for any type `α` that has a topology (i.e., it is a topological space) and for which the topology is discrete (i.e., every subset is open), any set `s` of elements of type `α` is a closed set. This means in such a space, it holds true that closure of any set is the set itself. The discrete topology is the finest topology you can put on a set, where every subset is open, and therefore, also closed.
More concisely: In a discrete topological space, every subset is closed.
|
Mathlib.Topology.Order._auxLemma.30
theorem Mathlib.Topology.Order._auxLemma.30 :
∀ {α : Type u_1} {β : Type u_2} {t : TopologicalSpace α} {s : Set β} {f : α → β}, IsOpen s = IsOpen (f ⁻¹' s) := by
sorry
This theorem states that for any two types `α` and `β`, a function `f` from `α` to `β`, and topological spaces `t₁` on `α` and `t₂` on `β`, the function `f` is continuous if and only if the topological space `t₁` is coarser (smaller or equal to) the topology induced on `α` by `f` and the topology `t₂` on `β`. In other words, `f` retains continuity when the topology on `α` is the coarsest topology that makes `f` continuous.
More concisely: A function between two topological spaces is continuous if and only if its domain is equipped with a coarser topology that makes the function continuous and the image topology is the given topology on the codomain.
|
eq_bot_of_singletons_open
theorem eq_bot_of_singletons_open : ∀ {α : Type u_1} {t : TopologicalSpace α}, (∀ (x : α), IsOpen {x}) → t = ⊥ := by
sorry
This theorem, "eq_bot_of_singletons_open", states that for any type `α` and for any topological space `t` defined on `α`, if every singleton set `{x}` where `x` is an element of `α`, is an open set in the topological space, then the topology `t` is equivalent to the trivial (or indiscrete) topology, denoted by `⊥`. The trivial topology is one where the only open sets are the empty set and the whole set. Hence, this result says that if singletons are open, the topology is as coarse as possible.
More concisely: If every singleton set is open in a topology, then the topology is equal to the trivial topology.
|
discreteTopology_iff_nhds
theorem discreteTopology_iff_nhds :
∀ {α : Type u_1} [inst : TopologicalSpace α], DiscreteTopology α ↔ ∀ (x : α), nhds x = pure x
This theorem characterizes discrete topological spaces as those in which every single point forms a neighborhood unto itself. More formally, for any type `α` with an associated topological space instance, the space is a discrete topology if and only if, for each element `x` of type `α`, the neighborhood of `x` (denoted as `nhds x`) is equivalent to the singleton set containing `x` (denoted as `pure x`).
More concisely: A topological space over type `α` is discrete if and only if for each `x` in `α`, the neighborhood of `x` is equivalent to the singleton set `{x}`.
|