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:
- a set which is relatively open in each
s ∈ S
is open; - a set which is relatively closed in each
s ∈ S
is closed; - for any topological space
Y
, a functionf : X → Y
is continuous provided that it is continuous on eachs ∈ S
.
We use the first condition as the definition
(see IsCoherentWith
in Mathlib/Topology/Defs/Induced.lean
),
and provide the others as corollaries.
Main results #
IsCoherentWith.of_seq
: ifX
is a sequential space andS
contains all sets of the forminsert x (Set.range u)
, whereu : ℕ → X
is a sequence that converges tox
, then we haveIsCoherentWith S
;
theorem
Topology.IsCoherentWith.isOpen_iff
{X : Type u_1}
[TopologicalSpace X]
{S : Set (Set X)}
{t : Set X}
(hS : IsCoherentWith S)
:
theorem
Topology.IsCoherentWith.isClosed_iff
{X : Type u_1}
[TopologicalSpace X]
{S : Set (Set X)}
{t : Set X}
(hS : IsCoherentWith S)
:
theorem
Topology.IsCoherentWith.continuous_iff
{X : Type u_1}
[TopologicalSpace X]
{S : Set (Set X)}
{Y : Type u_2}
[TopologicalSpace Y]
{f : X → Y}
(hS : IsCoherentWith S)
:
theorem
Topology.IsCoherentWith.of_continuous_prop
{X : Type u_1}
[TopologicalSpace X]
{S : Set (Set X)}
(h : ∀ (f : X → Prop), (∀ s ∈ S, ContinuousOn f s) → Continuous f)
:
theorem
Topology.IsCoherentWith.of_isClosed
{X : Type u_1}
[TopologicalSpace X]
{S : Set (Set X)}
(h : ∀ (t : Set X), (∀ s ∈ S, IsClosed (Subtype.val ⁻¹' t)) → IsClosed t)
:
theorem
Topology.IsCoherentWith.enlarge
{X : Type u_1}
[TopologicalSpace X]
{S T : Set (Set X)}
(hS : IsCoherentWith S)
(hT : ∀ s ∈ S, ∃ t ∈ T, s ⊆ t)
:
theorem
Topology.IsCoherentWith.mono
{X : Type u_1}
[TopologicalSpace X]
{S T : Set (Set X)}
(hS : IsCoherentWith S)
(hT : S ⊆ T)
:
theorem
Topology.IsCoherentWith.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
.
theorem
Topology.IsCoherentWith.of_nhds
{X : Type u_1}
[TopologicalSpace X]
{S : Set (Set X)}
(h : ∀ (x : X), ∃ s ∈ S, 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
.