Theorems · Definition · general topology

IsDenseInducing.extend

{α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      [inst : TopologicalSpace α] →
        [inst_1 : TopologicalSpace β] → {i : α → β} → [TopologicalSpace γ] → IsDenseInducing i → (α → γ) → β → γ

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.

Defined in

Mathlib.Topology.DenseEmbedding

Cited by

29 results in Mathlib

Foundations

Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpace