Documentation

Mathlib.Topology.RestrictGen

Topology generated by its restrictions to subsets #

We say that restrictions of the topology on X to sets from a family S generates the original topology, if either of the following equivalent conditions hold:

We use the first condition as the definition (see RestrictGenTopology in Mathlib/Topology/Defs/Induced.lean), and provide the others as corollaries.

Main results #

theorem RestrictGenTopology.isOpen_iff {X : Type u_1} [TopologicalSpace X] {S : Set (Set X)} {t : Set X} (hS : RestrictGenTopology S) :
IsOpen t sS, IsOpen (Subtype.val ⁻¹' t)
theorem RestrictGenTopology.isClosed_iff {X : Type u_1} [TopologicalSpace X] {S : Set (Set X)} {t : Set X} (hS : RestrictGenTopology S) :
IsClosed t sS, IsClosed (Subtype.val ⁻¹' t)
theorem RestrictGenTopology.continuous_iff {X : Type u_1} [TopologicalSpace X] {S : Set (Set X)} {Y : Type u_2} [TopologicalSpace Y] {f : XY} (hS : RestrictGenTopology S) :
Continuous f sS, ContinuousOn f s
theorem RestrictGenTopology.of_continuous_prop {X : Type u_1} [TopologicalSpace X] {S : Set (Set X)} (h : ∀ (f : XProp), (∀ sS, ContinuousOn f s)Continuous f) :
theorem RestrictGenTopology.of_isClosed {X : Type u_1} [TopologicalSpace X] {S : Set (Set X)} (h : ∀ (t : Set X), (∀ sS, IsClosed (Subtype.val ⁻¹' t))IsClosed t) :
theorem RestrictGenTopology.enlarge {X : Type u_1} [TopologicalSpace X] {S : Set (Set X)} {T : Set (Set X)} (hS : RestrictGenTopology S) (hT : sS, tT, s t) :
theorem RestrictGenTopology.mono {X : Type u_1} [TopologicalSpace X] {S : Set (Set X)} {T : Set (Set X)} (hS : RestrictGenTopology S) (hT : S T) :
theorem RestrictGenTopology.of_seq {X : Type u_1} [TopologicalSpace X] {S : Set (Set X)} [SequentialSpace X] (h : ∀ ⦃u : X⦄ ⦃x : X⦄, Filter.Tendsto u Filter.atTop (nhds x)insert x (Set.range u) S) :

If X is a sequential space and S contains each set of the form insert x (Set.range u) where u : ℕ → X is a sequence and x is its limit, then topology on X is generated by its restrictions to the sets of S.

A sequential space is compactly generated.

theorem RestrictGenTopology.of_nhds {X : Type u_1} [TopologicalSpace X] {S : Set (Set X)} (h : ∀ (x : X), sS, s nhds x) :

If each point of the space has a neighborhood from the family S, then the topology is generated by its restrictions to the sets of S.

A weakly locally compact space is compactly generated.