Theorems · Definition · general topology

Dense.extend

{α : Type u_1} →
  {β : Type u_2} → [inst : TopologicalSpace α] → [TopologicalSpace β] → {s : Set α} → Dense s → (↑s → β) → α → β

This is a shortcut for hs.isDenseInducing_val.extend f. It is useful because if s : Set α is dense then the coercion (↑) : s → α automatically satisfies IsUniformInducing and IsDenseInducing so this gives access to the theorems satisfied by a uniform extension by simply mentioning the density hypothesis.

Defined in

Mathlib.Topology.DenseEmbedding

Cited by

13 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace