This file defines three properties of functions:
dense_range f means f has dense image; dense_inducing i means i is also inducing; dense_embedding e means e is also an embedding.
The main theorem continuous_extend gives a criterion for a function f : X → Z to a regular (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 dense_inducing (not necessarily injective).
f : α → β has dense range if its range (image) is a dense subset of β.
If f : α → β has dense range and β contains some element, then α must too.
i : α → β is "dense inducing" if it has dense range and the topology on α is the one induced by i from the topology on β.
The product of two dense inducings is a dense inducing
γ -f→ α g↓ ↓e δ -h→ β
If i : α → β is a dense inducing, then any function f : α → γ "extends" to a function g = 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.
A dense embedding is an embedding with dense image.
The product of two dense embeddings is a dense embedding