Basic theory of topological spaces. #
The main definition is the type class TopologicalSpace X which endows a type X with a topology.
Then Set X gets predicates IsOpen, IsClosed and functions interior, closure and
frontier. Each point x of X gets a neighborhood filter 𝓝 x. A filter F on X has
x as a cluster point if ClusterPt x F : 𝓝 x ⊓ F ≠ ⊥. A map f : α → X clusters at x
along F : Filter α if MapClusterPt x F f : ClusterPt x (map f F). In particular
the notion of cluster point of a sequence u is MapClusterPt x atTop u.
For topological spaces X and Y, a function f : X → Y and a point x : X,
ContinuousAt f x means f is continuous at x, and global continuity is
Continuous f. There is also a version of continuity PContinuous for
partially defined functions.
Notation #
The following notation is introduced elsewhere and it heavily used in this file.
𝓝 x: the filternhds xof neighborhoods of a pointx;𝓟 s: the principal filter of a sets;𝓝[s] x: the filternhdsWithin x sof neighborhoods of a pointxwithin a sets;𝓝[≠] x: the filternhdsWithin x {x}ᶜof punctured neighborhoods ofx.
Implementation notes #
Topology in mathlib heavily uses filters (even more than in Bourbaki). See explanations in https://leanprover-community.github.io/theories/topology.html.
References #
- [N. Bourbaki, General Topology][bourbaki1966]
- [I. M. James, Topologies and Uniformities][james1999]
Tags #
topological space, interior, closure, frontier, neighborhood, continuity, continuous function
Topological spaces #
def
TopologicalSpace.ofClosed
{X : Type u}
(T : Set (Set X))
(empty_mem : ∅ ∈ T)
(sInter_mem : ∀ A ⊆ T, ⋂₀ A ∈ T)
(union_mem : ∀ A ∈ T, ∀ B ∈ T, A ∪ B ∈ T)
:
A constructor for topologies by specifying the closed sets, and showing that they satisfy the appropriate conditions.
Equations
- TopologicalSpace.ofClosed T empty_mem sInter_mem union_mem = { IsOpen := fun (X_1 : Set X) => X_1ᶜ ∈ T, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }
Instances For
theorem
isOpen_iUnion
{X : Type u}
{ι : Sort w}
[TopologicalSpace X]
{f : ι → Set X}
(h : ∀ (i : ι), IsOpen (f i))
:
IsOpen (⋃ (i : ι), f i)
theorem
isOpen_biUnion
{X : Type u}
{α : Type u_1}
[TopologicalSpace X]
{s : Set α}
{f : α → Set X}
(h : ∀ i ∈ s, IsOpen (f i))
:
IsOpen (⋃ i ∈ s, f i)
theorem
IsOpen.union
{X : Type u}
{s₁ : Set X}
{s₂ : Set X}
[TopologicalSpace X]
(h₁ : IsOpen s₁)
(h₂ : IsOpen s₂)
:
theorem
Set.Finite.isOpen_sInter
{X : Type u}
[TopologicalSpace X]
{s : Set (Set X)}
(hs : s.Finite)
:
theorem
Set.Finite.isOpen_biInter
{X : Type u}
{α : Type u_1}
[TopologicalSpace X]
{s : Set α}
{f : α → Set X}
(hs : s.Finite)
(h : ∀ i ∈ s, IsOpen (f i))
:
IsOpen (⋂ i ∈ s, f i)
theorem
isOpen_iInter_of_finite
{X : Type u}
{ι : Sort w}
[TopologicalSpace X]
[Finite ι]
{s : ι → Set X}
(h : ∀ (i : ι), IsOpen (s i))
:
IsOpen (⋂ (i : ι), s i)
theorem
isOpen_biInter_finset
{X : Type u}
{α : Type u_1}
[TopologicalSpace X]
{s : Finset α}
{f : α → Set X}
(h : ∀ i ∈ s, IsOpen (f i))
:
IsOpen (⋂ i ∈ s, f i)
@[simp]
@[simp]
theorem
TopologicalSpace.ext_iff_isClosed
{X : Type u_3}
{t₁ : TopologicalSpace X}
{t₂ : TopologicalSpace X}
:
theorem
TopologicalSpace.ext_isClosed
{X : Type u_3}
{t₁ : TopologicalSpace X}
{t₂ : TopologicalSpace X}
:
Alias of the reverse direction of TopologicalSpace.ext_iff_isClosed.
theorem
isClosed_iInter
{X : Type u}
{ι : Sort w}
[TopologicalSpace X]
{f : ι → Set X}
(h : ∀ (i : ι), IsClosed (f i))
:
IsClosed (⋂ (i : ι), f i)
theorem
isClosed_biInter
{X : Type u}
{α : Type u_1}
[TopologicalSpace X]
{s : Set α}
{f : α → Set X}
(h : ∀ i ∈ s, IsClosed (f i))
:
IsClosed (⋂ i ∈ s, f i)
@[simp]
Alias of the reverse direction of isClosed_compl_iff.
theorem
IsOpen.sdiff
{X : Type u}
{s : Set X}
{t : Set X}
[TopologicalSpace X]
(h₁ : IsOpen s)
(h₂ : IsClosed t)
:
theorem
IsClosed.inter
{X : Type u}
{s₁ : Set X}
{s₂ : Set X}
[TopologicalSpace X]
(h₁ : IsClosed s₁)
(h₂ : IsClosed s₂)
:
theorem
IsClosed.sdiff
{X : Type u}
{s : Set X}
{t : Set X}
[TopologicalSpace X]
(h₁ : IsClosed s)
(h₂ : IsOpen t)
:
theorem
Set.Finite.isClosed_biUnion
{X : Type u}
{α : Type u_1}
[TopologicalSpace X]
{s : Set α}
{f : α → Set X}
(hs : s.Finite)
(h : ∀ i ∈ s, IsClosed (f i))
:
IsClosed (⋃ i ∈ s, f i)
theorem
isClosed_biUnion_finset
{X : Type u}
{α : Type u_1}
[TopologicalSpace X]
{s : Finset α}
{f : α → Set X}
(h : ∀ i ∈ s, IsClosed (f i))
:
IsClosed (⋃ i ∈ s, f i)
theorem
isClosed_iUnion_of_finite
{X : Type u}
{ι : Sort w}
[TopologicalSpace X]
[Finite ι]
{s : ι → Set X}
(h : ∀ (i : ι), IsClosed (s i))
:
IsClosed (⋃ (i : ι), s i)
theorem
isClosed_imp
{X : Type u}
[TopologicalSpace X]
{p : X → Prop}
{q : X → Prop}
(hp : IsOpen {x : X | p x})
(hq : IsClosed {x : X | q x})
:
IsClosed {x : X | p x → q x}
Interior of a set #
@[simp]
theorem
interior_maximal
{X : Type u}
{s : Set X}
{t : Set X}
[TopologicalSpace X]
(h₁ : t ⊆ s)
(h₂ : IsOpen t)
:
@[simp]
@[simp]
theorem
Set.Finite.interior_biInter
{X : Type u}
[TopologicalSpace X]
{ι : Type u_3}
{s : Set ι}
(hs : s.Finite)
(f : ι → Set X)
:
theorem
Set.Finite.interior_sInter
{X : Type u}
[TopologicalSpace X]
{S : Set (Set X)}
(hS : S.Finite)
:
@[simp]
theorem
Finset.interior_iInter
{X : Type u}
[TopologicalSpace X]
{ι : Type u_3}
(s : Finset ι)
(f : ι → Set X)
:
@[simp]
theorem
interior_iInter_of_finite
{X : Type u}
{ι : Sort w}
[TopologicalSpace X]
[Finite ι]
(f : ι → Set X)
:
theorem
interior_iInter₂_subset
{X : Type u}
{ι : Sort w}
[TopologicalSpace X]
(p : ι → Sort u_3)
(s : (i : ι) → p i → Set X)
:
theorem
Filter.HasBasis.lift'_interior
{X : Type u}
{ι : Sort w}
[TopologicalSpace X]
{l : Filter X}
{p : ι → Prop}
{s : ι → Set X}
(h : l.HasBasis p s)
:
(l.lift' interior).HasBasis p fun (i : ι) => interior (s i)
theorem
Filter.lift'_interior_le
{X : Type u}
[TopologicalSpace X]
(l : Filter X)
:
l.lift' interior ≤ l
theorem
Filter.HasBasis.lift'_interior_eq_self
{X : Type u}
{ι : Sort w}
[TopologicalSpace X]
{l : Filter X}
{p : ι → Prop}
{s : ι → Set X}
(h : l.HasBasis p s)
(ho : ∀ (i : ι), p i → IsOpen (s i))
:
l.lift' interior = l
Closure of a set #
@[simp]
theorem
not_mem_of_not_mem_closure
{X : Type u}
{s : Set X}
[TopologicalSpace X]
{P : X}
(hP : P ∉ closure s)
:
P ∉ s
theorem
closure_minimal
{X : Type u}
{s : Set X}
{t : Set X}
[TopologicalSpace X]
(h₁ : s ⊆ t)
(h₂ : IsClosed t)
:
theorem
Disjoint.closure_left
{X : Type u}
{s : Set X}
{t : Set X}
[TopologicalSpace X]
(hd : Disjoint s t)
(ht : IsOpen t)
:
theorem
Disjoint.closure_right
{X : Type u}
{s : Set X}
{t : Set X}
[TopologicalSpace X]
(hd : Disjoint s t)
(hs : IsOpen s)
:
theorem
IsClosed.mem_iff_closure_subset
{X : Type u}
{x : X}
{s : Set X}
[TopologicalSpace X]
(hs : IsClosed s)
:
theorem
isClosed_of_closure_subset
{X : Type u}
{s : Set X}
[TopologicalSpace X]
(h : closure s ⊆ s)
:
IsClosed s
@[simp]
theorem
Set.Nonempty.of_closure
{X : Type u}
{s : Set X}
[TopologicalSpace X]
:
(closure s).Nonempty → s.Nonempty
Alias of the forward direction of closure_nonempty_iff.
theorem
Set.Nonempty.closure
{X : Type u}
{s : Set X}
[TopologicalSpace X]
:
s.Nonempty → (closure s).Nonempty
Alias of the reverse direction of closure_nonempty_iff.
@[simp]
theorem
Set.Finite.closure_biUnion
{X : Type u}
[TopologicalSpace X]
{ι : Type u_3}
{s : Set ι}
(hs : s.Finite)
(f : ι → Set X)
:
theorem
Set.Finite.closure_sUnion
{X : Type u}
[TopologicalSpace X]
{S : Set (Set X)}
(hS : S.Finite)
:
@[simp]
theorem
Finset.closure_biUnion
{X : Type u}
[TopologicalSpace X]
{ι : Type u_3}
(s : Finset ι)
(f : ι → Set X)
:
@[simp]
theorem
closure_iUnion_of_finite
{X : Type u}
{ι : Sort w}
[TopologicalSpace X]
[Finite ι]
(f : ι → Set X)
:
@[simp]
@[simp]
theorem
Filter.le_lift'_closure
{X : Type u}
[TopologicalSpace X]
(l : Filter X)
:
l ≤ l.lift' closure
theorem
Filter.HasBasis.lift'_closure
{X : Type u}
{ι : Sort w}
[TopologicalSpace X]
{l : Filter X}
{p : ι → Prop}
{s : ι → Set X}
(h : l.HasBasis p s)
:
(l.lift' closure).HasBasis p fun (i : ι) => closure (s i)
theorem
Filter.HasBasis.lift'_closure_eq_self
{X : Type u}
{ι : Sort w}
[TopologicalSpace X]
{l : Filter X}
{p : ι → Prop}
{s : ι → Set X}
(h : l.HasBasis p s)
(hc : ∀ (i : ι), p i → IsClosed (s i))
:
l.lift' closure = l
@[simp]
Alias of the forward direction of dense_iff_closure_eq.
@[simp]
The closure of a set s is dense if and only if s is dense.
Alias of the reverse direction of dense_closure.
The closure of a set s is dense if and only if s is dense.
Alias of the forward direction of dense_closure.
The closure of a set s is dense if and only if s is dense.
A set is dense if and only if it has a nonempty intersection with each nonempty open set.
Alias of the forward direction of dense_iff_inter_open.
A set is dense if and only if it has a nonempty intersection with each nonempty open set.
theorem
Dense.exists_mem_open
{X : Type u}
{s : Set X}
[TopologicalSpace X]
(hs : Dense s)
{U : Set X}
(ho : IsOpen U)
(hne : U.Nonempty)
:
∃ x ∈ s, x ∈ U
theorem
Dense.nonempty
{X : Type u}
{s : Set X}
[TopologicalSpace X]
[h : Nonempty X]
(hs : Dense s)
:
s.Nonempty
theorem
Dense.mono
{X : Type u}
{s₁ : Set X}
{s₂ : Set X}
[TopologicalSpace X]
(h : s₁ ⊆ s₂)
(hd : Dense s₁)
:
Dense s₂
Complement to a singleton is dense if and only if the singleton is not an open set.
theorem
IsOpen.subset_interior_closure
{X : Type u}
[TopologicalSpace X]
{s : Set X}
(s_open : IsOpen s)
:
theorem
IsClosed.closure_interior_subset
{X : Type u}
[TopologicalSpace X]
{s : Set X}
(s_closed : IsClosed s)
:
Frontier of a set #
@[simp]
Interior and frontier are disjoint.
@[simp]
@[simp]
Alias of the reverse direction of frontier_subset_iff_isClosed.
@[simp]
The complement of a set has the same frontier as the original set.
The frontier of a set is closed.
The frontier of a closed set has no interior point.
theorem
Disjoint.frontier_left
{X : Type u}
{s : Set X}
{t : Set X}
[TopologicalSpace X]
(ht : IsOpen t)
(hd : Disjoint s t)
:
theorem
Disjoint.frontier_right
{X : Type u}
{s : Set X}
{t : Set X}
[TopologicalSpace X]
(hs : IsOpen s)
(hd : Disjoint s t)
:
Neighborhoods #
The open sets containing x are a basis for the neighborhood filter. See nhds_basis_opens'
for a variant using open neighborhoods instead.
@[simp]
theorem
Filter.HasBasis.nhds_interior
{X : Type u}
{ι : Sort w}
[TopologicalSpace X]
{x : X}
{p : ι → Prop}
{s : ι → Set X}
(h : (nhds x).HasBasis p s)
:
theorem
nhds_le_of_le
{X : Type u}
{x : X}
{s : Set X}
[TopologicalSpace X]
{f : Filter X}
(h : x ∈ s)
(o : IsOpen s)
(sf : Filter.principal s ≤ f)
:
To show a filter is above the neighborhood filter at x, it suffices to show that it is above
the principal filter of some open set s containing x.
theorem
map_nhds
{X : Type u}
{α : Type u_1}
{x : X}
[TopologicalSpace X]
{f : X → α}
:
Filter.map f (nhds x) = ⨅ s ∈ {s : Set X | x ∈ s ∧ IsOpen s}, Filter.principal (f '' s)
theorem
Filter.Eventually.self_of_nhds
{X : Type u}
{x : X}
[TopologicalSpace X]
{p : X → Prop}
(h : ∀ᶠ (y : X) in nhds x, p y)
:
p x
If a predicate is true in a neighborhood of x, then it is true for x.
theorem
IsOpen.mem_nhds
{X : Type u}
{x : X}
{s : Set X}
[TopologicalSpace X]
(hs : IsOpen s)
(hx : x ∈ s)
:
theorem
IsClosed.compl_mem_nhds
{X : Type u}
{x : X}
{s : Set X}
[TopologicalSpace X]
(hs : IsClosed s)
(hx : x ∉ s)
:
theorem
IsOpen.eventually_mem
{X : Type u}
{x : X}
{s : Set X}
[TopologicalSpace X]
(hs : IsOpen s)
(hx : x ∈ s)
:
The open neighborhoods of x are a basis for the neighborhood filter. See nhds_basis_opens
for a variant using open sets around x instead.
theorem
Filter.Eventually.eventually_nhds
{X : Type u}
{x : X}
[TopologicalSpace X]
{p : X → Prop}
(h : ∀ᶠ (y : X) in nhds x, p y)
:
If a predicate is true in a neighbourhood of x, then for y sufficiently close
to x this predicate is true in a neighbourhood of y.
@[simp]
@[simp]
@[deprecated eventually_mem_nhds_iff]
Alias of eventually_mem_nhds_iff.
@[simp]
theorem
Filter.EventuallyEq.eq_of_nhds
{X : Type u}
{α : Type u_1}
{x : X}
[TopologicalSpace X]
{f : X → α}
{g : X → α}
(h : f =ᶠ[nhds x] g)
:
f x = g x
theorem
Filter.EventuallyEq.eventuallyEq_nhds
{X : Type u}
{α : Type u_1}
{x : X}
[TopologicalSpace X]
{f : X → α}
{g : X → α}
(h : f =ᶠ[nhds x] g)
:
If two functions are equal in a neighbourhood of x, then for y sufficiently close
to x these functions are equal in a neighbourhood of y.
theorem
Filter.EventuallyLE.eventuallyLE_nhds
{X : Type u}
{α : Type u_1}
{x : X}
[TopologicalSpace X]
[LE α]
{f : X → α}
{g : X → α}
(h : f ≤ᶠ[nhds x] g)
:
If f x ≤ g x in a neighbourhood of x, then for y sufficiently close to x we have
f x ≤ g x in a neighbourhood of y.
theorem
tendsto_nhds
{X : Type u}
{α : Type u_1}
{x : X}
[TopologicalSpace X]
{f : α → X}
{l : Filter α}
:
theorem
tendsto_atTop_nhds
{X : Type u}
{α : Type u_1}
{x : X}
[TopologicalSpace X]
[Nonempty α]
[SemilatticeSup α]
{f : α → X}
:
theorem
tendsto_const_nhds
{X : Type u}
{α : Type u_1}
{x : X}
[TopologicalSpace X]
{f : Filter α}
:
Filter.Tendsto (fun (x_1 : α) => x) f (nhds x)
theorem
tendsto_atTop_of_eventually_const
{X : Type u}
{x : X}
[TopologicalSpace X]
{ι : Type u_3}
[Preorder ι]
{u : ι → X}
{i₀ : ι}
(h : ∀ i ≥ i₀, u i = x)
:
Filter.Tendsto u Filter.atTop (nhds x)
theorem
tendsto_atBot_of_eventually_const
{X : Type u}
{x : X}
[TopologicalSpace X]
{ι : Type u_3}
[Preorder ι]
{u : ι → X}
{i₀ : ι}
(h : ∀ i ≤ i₀, u i = x)
:
Filter.Tendsto u Filter.atBot (nhds x)
theorem
tendsto_pure_nhds
{X : Type u}
{α : Type u_1}
[TopologicalSpace X]
(f : α → X)
(a : α)
:
Filter.Tendsto f (pure a) (nhds (f a))
theorem
OrderTop.tendsto_atTop_nhds
{X : Type u}
{α : Type u_1}
[TopologicalSpace X]
[PartialOrder α]
[OrderTop α]
(f : α → X)
:
Filter.Tendsto f Filter.atTop (nhds (f ⊤))
@[simp]
Equations
- ⋯ = ⋯
theorem
tendsto_nhds_of_eventually_eq
{X : Type u}
{α : Type u_1}
{x : X}
[TopologicalSpace X]
{l : Filter α}
{f : α → X}
(h : ∀ᶠ (x' : α) in l, f x' = x)
:
Filter.Tendsto f l (nhds x)
theorem
Filter.EventuallyEq.tendsto
{X : Type u}
{α : Type u_1}
{x : X}
[TopologicalSpace X]
{l : Filter α}
{f : α → X}
(hf : f =ᶠ[l] fun (x_1 : α) => x)
:
Filter.Tendsto f l (nhds x)
Cluster points #
In this section we define cluster points (also known as limit points and accumulation points) of a filter and of a sequence.
theorem
ClusterPt.neBot
{X : Type u}
{x : X}
[TopologicalSpace X]
{F : Filter X}
(h : ClusterPt x F)
:
theorem
clusterPt_principal_iff
{X : Type u}
{x : X}
{s : Set X}
[TopologicalSpace X]
:
ClusterPt x (Filter.principal s) ↔ ∀ U ∈ nhds x, (U ∩ s).Nonempty
x is a cluster point of a set s if every neighbourhood of x meets s on a nonempty
set. See also mem_closure_iff_clusterPt.
theorem
clusterPt_principal_iff_frequently
{X : Type u}
{x : X}
{s : Set X}
[TopologicalSpace X]
:
ClusterPt x (Filter.principal s) ↔ ∃ᶠ (y : X) in nhds x, y ∈ s
theorem
ClusterPt.of_le_nhds
{X : Type u}
{x : X}
[TopologicalSpace X]
{f : Filter X}
(H : f ≤ nhds x)
[f.NeBot]
:
ClusterPt x f
theorem
ClusterPt.of_le_nhds'
{X : Type u}
{x : X}
[TopologicalSpace X]
{f : Filter X}
(H : f ≤ nhds x)
(_hf : f.NeBot)
:
ClusterPt x f
theorem
ClusterPt.of_nhds_le
{X : Type u}
{x : X}
[TopologicalSpace X]
{f : Filter X}
(H : nhds x ≤ f)
:
ClusterPt x f
theorem
ClusterPt.mono
{X : Type u}
{x : X}
[TopologicalSpace X]
{f : Filter X}
{g : Filter X}
(H : ClusterPt x f)
(h : f ≤ g)
:
ClusterPt x g
theorem
ClusterPt.of_inf_left
{X : Type u}
{x : X}
[TopologicalSpace X]
{f : Filter X}
{g : Filter X}
(H : ClusterPt x (f ⊓ g))
:
ClusterPt x f
theorem
ClusterPt.of_inf_right
{X : Type u}
{x : X}
[TopologicalSpace X]
{f : Filter X}
{g : Filter X}
(H : ClusterPt x (f ⊓ g))
:
ClusterPt x g
theorem
mapClusterPt_def
{X : Type u}
{α : Type u_1}
[TopologicalSpace X]
{F : Filter α}
{u : α → X}
{x : X}
:
MapClusterPt x F u ↔ ClusterPt x (Filter.map u F)
theorem
MapClusterPt.clusterPt
{X : Type u}
{α : Type u_1}
[TopologicalSpace X]
{F : Filter α}
{u : α → X}
{x : X}
:
MapClusterPt x F u → ClusterPt x (Filter.map u F)
Alias of the forward direction of mapClusterPt_def.
theorem
MapClusterPt.mono
{X : Type u}
{α : Type u_1}
[TopologicalSpace X]
{F : Filter α}
{u : α → X}
{x : X}
{G : Filter α}
(h : MapClusterPt x F u)
(hle : F ≤ G)
:
MapClusterPt x G u
theorem
MapClusterPt.tendsto_comp'
{X : Type u}
{Y : Type v}
{α : Type u_1}
[TopologicalSpace X]
{F : Filter α}
{u : α → X}
{x : X}
[TopologicalSpace Y]
{f : X → Y}
{y : Y}
(hf : Filter.Tendsto f (nhds x ⊓ Filter.map u F) (nhds y))
(hu : MapClusterPt x F u)
:
MapClusterPt y F (f ∘ u)
theorem
MapClusterPt.tendsto_comp
{X : Type u}
{Y : Type v}
{α : Type u_1}
[TopologicalSpace X]
{F : Filter α}
{u : α → X}
{x : X}
[TopologicalSpace Y]
{f : X → Y}
{y : Y}
(hf : Filter.Tendsto f (nhds x) (nhds y))
(hu : MapClusterPt x F u)
:
MapClusterPt y F (f ∘ u)
theorem
MapClusterPt.continuousAt_comp
{X : Type u}
{Y : Type v}
{α : Type u_1}
[TopologicalSpace X]
{F : Filter α}
{u : α → X}
{x : X}
[TopologicalSpace Y]
{f : X → Y}
(hf : ContinuousAt f x)
(hu : MapClusterPt x F u)
:
MapClusterPt (f x) F (f ∘ u)
theorem
Filter.HasBasis.mapClusterPt_iff_frequently
{X : Type u}
{α : Type u_1}
[TopologicalSpace X]
{F : Filter α}
{u : α → X}
{x : X}
{ι : Sort u_3}
{p : ι → Prop}
{s : ι → Set X}
(hx : (nhds x).HasBasis p s)
:
MapClusterPt x F u ↔ ∀ (i : ι), p i → ∃ᶠ (a : α) in F, u a ∈ s i
theorem
mapClusterPt_iff
{X : Type u}
{α : Type u_1}
[TopologicalSpace X]
{F : Filter α}
{u : α → X}
{x : X}
:
MapClusterPt x F u ↔ ∀ s ∈ nhds x, ∃ᶠ (a : α) in F, u a ∈ s
theorem
mapClusterPt_iff_ultrafilter
{X : Type u}
{α : Type u_1}
[TopologicalSpace X]
{F : Filter α}
{u : α → X}
{x : X}
:
MapClusterPt x F u ↔ ∃ (U : Ultrafilter α), ↑U ≤ F ∧ Filter.Tendsto u (↑U) (nhds x)
theorem
mapClusterPt_comp
{X : Type u}
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace X]
{F : Filter α}
{x : X}
{φ : α → β}
{u : β → X}
:
MapClusterPt x F (u ∘ φ) ↔ MapClusterPt x (Filter.map φ F) u
theorem
Filter.Tendsto.mapClusterPt
{X : Type u}
{α : Type u_1}
[TopologicalSpace X]
{F : Filter α}
{u : α → X}
{x : X}
[F.NeBot]
(h : Filter.Tendsto u F (nhds x))
:
MapClusterPt x F u
theorem
MapClusterPt.of_comp
{X : Type u}
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace X]
{F : Filter α}
{u : α → X}
{x : X}
{φ : β → α}
{p : Filter β}
(h : Filter.Tendsto φ p F)
(H : MapClusterPt x p (u ∘ φ))
:
MapClusterPt x F u
@[deprecated MapClusterPt.of_comp]
theorem
mapClusterPt_of_comp
{X : Type u}
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace X]
{F : Filter α}
{u : α → X}
{x : X}
{φ : β → α}
{p : Filter β}
[p.NeBot]
(h : Filter.Tendsto φ p F)
(H : Filter.Tendsto (u ∘ φ) p (nhds x))
:
MapClusterPt x F u
theorem
acc_principal_iff_cluster
{X : Type u}
[TopologicalSpace X]
(x : X)
(C : Set X)
:
AccPt x (Filter.principal C) ↔ ClusterPt x (Filter.principal (C \ {x}))
x is an accumulation point of a set C iff it is a cluster point of C ∖ {x}.
x is an accumulation point of a set C iff every neighborhood
of x contains a point of C other than x.
x is an accumulation point of a set C iff
there are points near x in C and different from x.
theorem
AccPt.mono
{X : Type u}
{x : X}
[TopologicalSpace X]
{F : Filter X}
{G : Filter X}
(h : AccPt x F)
(hFG : F ≤ G)
:
AccPt x G
If x is an accumulation point of F and F ≤ G, then
x is an accumulation point of G.
theorem
AccPt.clusterPt
{X : Type u}
[TopologicalSpace X]
(x : X)
(F : Filter X)
(h : AccPt x F)
:
ClusterPt x F
theorem
clusterPt_principal
{X : Type u}
[TopologicalSpace X]
{x : X}
{C : Set X}
:
ClusterPt x (Filter.principal C) ↔ x ∈ C ∨ AccPt x (Filter.principal C)
Interior, closure and frontier in terms of neighborhoods #
theorem
interior_eq_nhds
{X : Type u}
{s : Set X}
[TopologicalSpace X]
:
interior s = {x : X | nhds x ≤ Filter.principal s}
theorem
isOpen_iff_nhds
{X : Type u}
{s : Set X}
[TopologicalSpace X]
:
IsOpen s ↔ ∀ x ∈ s, nhds x ≤ Filter.principal s
theorem
TopologicalSpace.ext_iff_nhds
{X : Type u_3}
{t : TopologicalSpace X}
{t' : TopologicalSpace X}
:
theorem
TopologicalSpace.ext_nhds
{X : Type u_3}
{t : TopologicalSpace X}
{t' : TopologicalSpace X}
:
Alias of the reverse direction of TopologicalSpace.ext_iff_nhds.
A set s is open iff for every point x in s and every y close to x, y is in s.
Alias of the reverse direction of mem_closure_iff_frequently.
A set s is closed iff for every point x, if there is a point y close to x that belongs
to s then x is in s.
The set of cluster points of a filter is closed. In particular, the set of limit points of a sequence is closed.
theorem
mem_closure_iff_clusterPt
{X : Type u}
{x : X}
{s : Set X}
[TopologicalSpace X]
:
x ∈ closure s ↔ ClusterPt x (Filter.principal s)
@[deprecated mem_closure_iff_nhds_ne_bot]
Alias of mem_closure_iff_nhds_ne_bot.
theorem
mem_closure_iff_nhdsWithin_neBot
{X : Type u}
{x : X}
{s : Set X}
[TopologicalSpace X]
:
x ∈ closure s ↔ (nhdsWithin x s).NeBot
theorem
nhdsWithin_mono
{X : Type u}
[TopologicalSpace X]
(x : X)
{s : Set X}
{t : Set X}
(h : s ⊆ t)
:
nhdsWithin x s ≤ nhdsWithin x t
theorem
not_mem_closure_iff_nhdsWithin_eq_bot
{X : Type u}
{x : X}
{s : Set X}
[TopologicalSpace X]
:
x ∉ closure s ↔ nhdsWithin x s = ⊥
theorem
dense_compl_singleton
{X : Type u}
[TopologicalSpace X]
(x : X)
[(nhdsWithin x {x}ᶜ).NeBot]
:
If x is not an isolated point of a topological space, then {x}ᶜ is dense in the whole
space.
theorem
closure_compl_singleton
{X : Type u}
[TopologicalSpace X]
(x : X)
[(nhdsWithin x {x}ᶜ).NeBot]
:
If x is not an isolated point of a topological space, then the closure of {x}ᶜ is the whole
space.
@[simp]
If x is not an isolated point of a topological space, then the interior of {x} is empty.
theorem
not_isOpen_singleton
{X : Type u}
[TopologicalSpace X]
(x : X)
[(nhdsWithin x {x}ᶜ).NeBot]
:
theorem
closure_eq_cluster_pts
{X : Type u}
{s : Set X}
[TopologicalSpace X]
:
closure s = {a : X | ClusterPt a (Filter.principal s)}
theorem
mem_closure_iff_comap_neBot
{X : Type u}
{x : X}
{s : Set X}
[TopologicalSpace X]
:
x ∈ closure s ↔ (Filter.comap Subtype.val (nhds x)).NeBot
@[simp]
x belongs to the closure of s if and only if some ultrafilter
supported on s converges to x.
theorem
isClosed_iff_clusterPt
{X : Type u}
{s : Set X}
[TopologicalSpace X]
:
IsClosed s ↔ ∀ (a : X), ClusterPt a (Filter.principal s) → a ∈ s
theorem
Dense.inter_nhds_nonempty
{X : Type u}
{x : X}
{s : Set X}
{t : Set X}
[TopologicalSpace X]
(hs : Dense s)
(ht : t ∈ nhds x)
:
(s ∩ t).Nonempty
theorem
Filter.Frequently.mem_of_closed
{X : Type u}
{x : X}
{s : Set X}
[TopologicalSpace X]
(h : ∃ᶠ (x : X) in nhds x, x ∈ s)
(hs : IsClosed s)
:
x ∈ s
theorem
IsClosed.mem_of_frequently_of_tendsto
{X : Type u}
{α : Type u_1}
{x : X}
{s : Set X}
[TopologicalSpace X]
{f : α → X}
{b : Filter α}
(hs : IsClosed s)
(h : ∃ᶠ (x : α) in b, f x ∈ s)
(hf : Filter.Tendsto f b (nhds x))
:
x ∈ s
theorem
IsClosed.mem_of_tendsto
{X : Type u}
{α : Type u_1}
{x : X}
{s : Set X}
[TopologicalSpace X]
{f : α → X}
{b : Filter α}
[b.NeBot]
(hs : IsClosed s)
(hf : Filter.Tendsto f b (nhds x))
(h : ∀ᶠ (x : α) in b, f x ∈ s)
:
x ∈ s
theorem
mem_closure_of_frequently_of_tendsto
{X : Type u}
{α : Type u_1}
{x : X}
{s : Set X}
[TopologicalSpace X]
{f : α → X}
{b : Filter α}
(h : ∃ᶠ (x : α) in b, f x ∈ s)
(hf : Filter.Tendsto f b (nhds x))
:
theorem
mem_closure_of_tendsto
{X : Type u}
{α : Type u_1}
{x : X}
{s : Set X}
[TopologicalSpace X]
{f : α → X}
{b : Filter α}
[b.NeBot]
(hf : Filter.Tendsto f b (nhds x))
(h : ∀ᶠ (x : α) in b, f x ∈ s)
:
theorem
tendsto_inf_principal_nhds_iff_of_forall_eq
{X : Type u}
{α : Type u_1}
{x : X}
[TopologicalSpace X]
{f : α → X}
{l : Filter α}
{s : Set α}
(h : ∀ a ∉ s, f a = x)
:
Filter.Tendsto f (l ⊓ Filter.principal s) (nhds x) ↔ Filter.Tendsto f l (nhds x)
Suppose that f sends the complement to s to a single point x, and l is some filter.
Then f tends to x along l restricted to s if and only if it tends to x along l.
Limits of filters in topological spaces #
In this section we define functions that return a limit of a filter (or of a function along a
filter), if it exists, and a random point otherwise. These functions are rarely used in Mathlib,
most of the theorems are written using Filter.Tendsto. One of the reasons is that
Filter.limUnder f g = x is not equivalent to Filter.Tendsto g f (𝓝 x) unless the codomain is a
Hausdorff space and g has a limit along f.
If a filter f is majorated by some 𝓝 x, then it is majorated by 𝓝 (Filter.lim f). We
formulate this lemma with a [Nonempty X] argument of lim derived from h to make it useful for
types without a [Nonempty X] instance. Because of the built-in proof irrelevance, Lean will unify
this instance with any other instance.
theorem
tendsto_nhds_limUnder
{X : Type u}
{α : Type u_1}
[TopologicalSpace X]
{f : Filter α}
{g : α → X}
(h : ∃ (x : X), Filter.Tendsto g f (nhds x))
:
Filter.Tendsto g f (nhds (limUnder f g))
If g tends to some 𝓝 x along f, then it tends to 𝓝 (Filter.limUnder f g). We formulate
this lemma with a [Nonempty X] argument of lim derived from h to make it useful for types
without a [Nonempty X] instance. Because of the built-in proof irrelevance, Lean will unify this
instance with any other instance.
Continuity #
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)
theorem
IsOpen.preimage
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
(hf : Continuous f)
{t : Set Y}
(h : IsOpen t)
:
theorem
continuous_congr
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{g : X → Y}
(h : ∀ (x : X), f x = g x)
:
Continuous f ↔ Continuous g
theorem
Continuous.congr
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{g : X → Y}
(h : Continuous f)
(h' : ∀ (x : X), f x = g x)
:
theorem
ContinuousAt.tendsto
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{x : X}
(h : ContinuousAt f x)
:
Filter.Tendsto f (nhds x) (nhds (f x))
theorem
continuousAt_def
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{x : X}
:
theorem
continuousAt_congr
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{x : X}
{g : X → Y}
(h : f =ᶠ[nhds x] g)
:
ContinuousAt f x ↔ ContinuousAt g x
theorem
ContinuousAt.congr
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{x : X}
{g : X → Y}
(hf : ContinuousAt f x)
(h : f =ᶠ[nhds x] g)
:
ContinuousAt g x
theorem
ContinuousAt.preimage_mem_nhds
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{x : X}
{t : Set Y}
(h : ContinuousAt f x)
(ht : t ∈ nhds (f x))
:
theorem
ContinuousAt.eventually_mem
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{x : X}
(hf : ContinuousAt f x)
{s : Set Y}
(hs : s ∈ nhds (f x))
:
If f x ∈ s ∈ 𝓝 (f x) for continuous f, then f y ∈ s near x.
This is essentially Filter.Tendsto.eventually_mem, but infers in more cases when applied.
theorem
not_continuousAt_of_tendsto
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{l₁ : Filter X}
{l₂ : Filter Y}
{x : X}
(hf : Filter.Tendsto f l₁ l₂)
[l₁.NeBot]
(hl₁ : l₁ ≤ nhds x)
(hl₂ : Disjoint (nhds (f x)) l₂)
:
¬ContinuousAt f x
If a function f tends to somewhere other than 𝓝 (f x) at x,
then f is not continuous at x
@[deprecated]
theorem
eventuallyEq_zero_nhds
{X : Type u_1}
[TopologicalSpace X]
{x : X}
{M₀ : Type u_4}
[Zero M₀]
{f : X → M₀}
:
Deprecated, please use not_mem_tsupport_iff_eventuallyEq instead.
theorem
ClusterPt.map
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{x : X}
{lx : Filter X}
{ly : Filter Y}
(H : ClusterPt x lx)
(hfc : ContinuousAt f x)
(hf : Filter.Tendsto f lx ly)
:
ClusterPt (f x) ly
theorem
preimage_interior_subset_interior_preimage
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{t : Set Y}
(hf : Continuous f)
:
See also interior_preimage_subset_preimage_interior.
theorem
Continuous.comp
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : X → Y}
{g : Y → Z}
(hg : Continuous g)
(hf : Continuous f)
:
Continuous (g ∘ f)
theorem
Continuous.comp'
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : X → Y}
{g : Y → Z}
(hg : Continuous g)
(hf : Continuous f)
:
Continuous fun (x : X) => g (f x)
theorem
Continuous.iterate
{X : Type u_1}
[TopologicalSpace X]
{f : X → X}
(h : Continuous f)
(n : ℕ)
:
theorem
ContinuousAt.comp
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : X → Y}
{x : X}
{g : Y → Z}
(hg : ContinuousAt g (f x))
(hf : ContinuousAt f x)
:
ContinuousAt (g ∘ f) x
theorem
ContinuousAt.comp'
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : X → Y}
{g : Y → Z}
{x : X}
(hg : ContinuousAt g (f x))
(hf : ContinuousAt f x)
:
ContinuousAt (fun (x : X) => g (f x)) x
theorem
ContinuousAt.comp_of_eq
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : X → Y}
{x : X}
{y : Y}
{g : Y → Z}
(hg : ContinuousAt g y)
(hf : ContinuousAt f x)
(hy : f x = y)
:
ContinuousAt (g ∘ f) x
See note [comp_of_eq lemmas]
theorem
Continuous.tendsto
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
(hf : Continuous f)
(x : X)
:
Filter.Tendsto f (nhds x) (nhds (f x))
theorem
Continuous.tendsto'
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
(hf : Continuous f)
(x : X)
(y : Y)
(h : f x = y)
:
Filter.Tendsto f (nhds x) (nhds y)
A version of Continuous.tendsto that allows one to specify a simpler form of the limit.
E.g., one can write continuous_exp.tendsto' 0 1 exp_zero.
theorem
Continuous.continuousAt
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{x : X}
(h : Continuous f)
:
ContinuousAt f x
theorem
continuous_iff_continuousAt
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
:
Continuous f ↔ ∀ (x : X), ContinuousAt f x
theorem
continuousAt_const
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{x : X}
{y : Y}
:
ContinuousAt (fun (x : X) => y) x
theorem
continuous_const
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{y : Y}
:
Continuous fun (x : X) => y
theorem
Filter.EventuallyEq.continuousAt
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{x : X}
{y : Y}
(h : f =ᶠ[nhds x] fun (x : X) => y)
:
ContinuousAt f x
theorem
continuous_of_const
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
(h : ∀ (x y : X), f x = f y)
:
theorem
continuousAt_id'
{X : Type u_1}
[TopologicalSpace X]
(y : X)
:
ContinuousAt (fun (x : X) => x) y
theorem
ContinuousAt.iterate
{X : Type u_1}
[TopologicalSpace X]
{x : X}
{f : X → X}
(hf : ContinuousAt f x)
(hx : f x = x)
(n : ℕ)
:
ContinuousAt f^[n] x
theorem
continuous_iff_isClosed
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
:
theorem
IsClosed.preimage
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
(hf : Continuous f)
{t : Set Y}
(h : IsClosed t)
:
theorem
mem_closure_image
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{s : Set X}
{x : X}
(hf : ContinuousAt f x)
(hx : x ∈ closure s)
:
theorem
continuousAt_iff_ultrafilter
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{x : X}
:
ContinuousAt f x ↔ ∀ (g : Ultrafilter X), ↑g ≤ nhds x → Filter.Tendsto f (↑g) (nhds (f x))
theorem
continuous_iff_ultrafilter
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
:
Continuous f ↔ ∀ (x : X) (g : Ultrafilter X), ↑g ≤ nhds x → Filter.Tendsto f (↑g) (nhds (f x))
theorem
Continuous.closure_preimage_subset
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
(hf : Continuous f)
(t : Set Y)
:
theorem
Continuous.frontier_preimage_subset
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
(hf : Continuous f)
(t : Set Y)
:
theorem
Set.MapsTo.closure
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{s : Set X}
{t : Set Y}
(h : Set.MapsTo f s t)
(hc : Continuous f)
:
Set.MapsTo f (closure s) (closure t)
If a continuous map f maps s to t, then it maps closure s to closure t.
theorem
image_closure_subset_closure_image
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{s : Set X}
(h : Continuous f)
:
See also IsClosedMap.closure_image_eq_of_continuous.
theorem
closure_image_closure
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{s : Set X}
(h : Continuous f)
:
theorem
closure_subset_preimage_closure_image
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{s : Set X}
(h : Continuous f)
:
theorem
map_mem_closure
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{s : Set X}
{x : X}
{t : Set Y}
(hf : Continuous f)
(hx : x ∈ closure s)
(ht : Set.MapsTo f s t)
:
theorem
Set.MapsTo.closure_left
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{s : Set X}
{t : Set Y}
(h : Set.MapsTo f s t)
(hc : Continuous f)
(ht : IsClosed t)
:
Set.MapsTo f (closure s) t
If a continuous map f maps s to a closed set t, then it maps closure s to t.
theorem
Filter.Tendsto.lift'_closure
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
(hf : Continuous f)
{l : Filter X}
{l' : Filter Y}
(h : Filter.Tendsto f l l')
:
Filter.Tendsto f (l.lift' closure) (l'.lift' closure)
theorem
tendsto_lift'_closure_nhds
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
(hf : Continuous f)
(x : X)
:
Filter.Tendsto f ((nhds x).lift' closure) ((nhds (f x)).lift' closure)
Function with dense range #
theorem
Function.Surjective.denseRange
{X : Type u_1}
[TopologicalSpace X]
{α : Type u_4}
{f : α → X}
(hf : Function.Surjective f)
:
A surjective map has dense range.
theorem
denseRange_iff_closure_range
{X : Type u_1}
[TopologicalSpace X]
{α : Type u_4}
{f : α → X}
:
DenseRange f ↔ closure (Set.range f) = Set.univ
theorem
DenseRange.closure_range
{X : Type u_1}
[TopologicalSpace X]
{α : Type u_4}
{f : α → X}
(h : DenseRange f)
:
@[simp]
theorem
denseRange_subtype_val
{X : Type u_1}
[TopologicalSpace X]
{p : X → Prop}
:
DenseRange Subtype.val ↔ Dense {x : X | p x}
theorem
Dense.denseRange_val
{X : Type u_1}
[TopologicalSpace X]
{s : Set X}
(h : Dense s)
:
DenseRange Subtype.val
theorem
Continuous.range_subset_closure_image_dense
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{s : Set X}
{f : X → Y}
(hf : Continuous f)
(hs : Dense s)
:
theorem
DenseRange.dense_image
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{s : Set X}
{f : X → Y}
(hf' : DenseRange f)
(hf : Continuous f)
(hs : Dense s)
:
The image of a dense set under a continuous map with dense range is a dense set.
theorem
DenseRange.subset_closure_image_preimage_of_isOpen
{X : Type u_1}
[TopologicalSpace X]
{α : Type u_4}
{f : α → X}
{s : Set X}
(hf : DenseRange f)
(hs : IsOpen s)
:
If f has dense range and s is an open set in the codomain of f, then the image of the
preimage of s under f is dense in s.
theorem
DenseRange.dense_of_mapsTo
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{s : Set X}
{f : X → Y}
(hf' : DenseRange f)
(hf : Continuous f)
(hs : Dense s)
{t : Set Y}
(ht : Set.MapsTo f s t)
:
Dense t
If a continuous map with dense range maps a dense set to a subset of t, then t is a dense
set.
theorem
DenseRange.comp
{Y : Type u_2}
{Z : Type u_3}
[TopologicalSpace Y]
[TopologicalSpace Z]
{α : Type u_4}
{g : Y → Z}
{f : α → Y}
(hg : DenseRange g)
(hf : DenseRange f)
(cg : Continuous g)
:
DenseRange (g ∘ f)
Composition of a continuous map with dense range and a function with dense range has dense range.
theorem
DenseRange.nonempty_iff
{X : Type u_1}
[TopologicalSpace X]
{α : Type u_4}
{f : α → X}
(hf : DenseRange f)
:
theorem
DenseRange.nonempty
{X : Type u_1}
[TopologicalSpace X]
{α : Type u_4}
{f : α → X}
[h : Nonempty X]
(hf : DenseRange f)
:
Nonempty α
def
DenseRange.some
{X : Type u_1}
[TopologicalSpace X]
{α : Type u_4}
{f : α → X}
(hf : DenseRange f)
(x : X)
:
α
Given a function f : X → Y with dense range and y : Y, returns some x : X.
Equations
- hf.some x = Classical.choice ⋯
Instances For
theorem
DenseRange.exists_mem_open
{X : Type u_1}
[TopologicalSpace X]
{α : Type u_4}
{f : α → X}
{s : Set X}
(hf : DenseRange f)
(ho : IsOpen s)
(hs : s.Nonempty)
:
∃ (a : α), f a ∈ s
theorem
DenseRange.mem_nhds
{X : Type u_1}
[TopologicalSpace X]
{x : X}
{α : Type u_4}
{f : α → X}
{s : Set X}
(h : DenseRange f)
(hs : s ∈ nhds x)
:
∃ (a : α), f a ∈ s