Dense embeddings #
This file defines three properties of functions:
DenseRange f
meansf
has dense image;IsDenseInducing i
meansi
is alsoInducing
, namely it induces the topology on its codomain;IsDenseEmbedding e
meanse
is further anEmbedding
, namely it is injective andInducing
.
The main theorem continuous_extend
gives a criterion for a function
f : X → Z
to a T₃ space Z to extend along a dense embedding
i : X → Y
to a continuous function g : Y → Z
. Actually i
only
has to be IsDenseInducing
(not necessarily injective).
i : α → β
is "dense inducing" if it has dense range and the topology on α
is the one induced by i
from the topology on β
.
- induced : inst✝¹ = TopologicalSpace.induced i inst✝
- dense : DenseRange i
The range of a dense inducing map is a dense set.
Instances For
The range of a dense inducing map is a dense set.
If i : α → β
is a dense embedding with dense complement of the range, then any compact set in
α
has empty interior.
The product of two dense inducings is a dense inducing
If the domain of a IsDenseInducing
map is a separable space, then so is the codomain.
γ -f→ α
g↓ ↓e
δ -h→ β
If i : α → β
is a dense inducing, then any function f : α → γ
"extends" to a function g = IsDenseInducing.extend di f : β → γ
. If γ
is Hausdorff and f
has a continuous extension, then
g
is the unique such extension. In general, g
might not be continuous or even extend f
.
Equations
- di.extend f b = limUnder (Filter.comap i (nhds b)) f
Instances For
Variation of extend_eq
where we ask that f
has a limit along comap i (𝓝 b)
for each
b : β
. This is a strictly stronger assumption than continuity of f
, but in a lot of cases
you'd have to prove it anyway to use continuous_extend
, so this avoids doing the work twice.
A dense embedding is an embedding with dense image.
- induced : inst✝¹ = TopologicalSpace.induced e inst✝
- dense : DenseRange e
- inj : Function.Injective e
A dense embedding is injective.
Instances For
A dense embedding is injective.
Alias of IsDenseEmbedding.mk'
.
If the domain of a IsDenseEmbedding
is a separable space, then so is its codomain.
The product of two dense embeddings is a dense embedding.
The dense embedding of a subtype inside its closure.
Equations
- IsDenseEmbedding.subtypeEmb p e x = ⟨e ↑x, ⋯⟩
Instances For
Alias of IsDenseEmbedding.id
.
Alias of Dense.isDenseEmbedding_val
.
Two continuous functions to a t2-space that agree on the dense range of a function are equal.