Theorems · Inductive type · general topology

IsDenseInducing

{α : Type u_1} → {β : Type u_2} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop

i : α → β is "dense inducing" if it has dense range and the topology on α is the one induced by i from the topology on β.

Defined in

Mathlib.Topology.DenseEmbedding

Cited by

56 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopologicalSpace