Documentation

BrownianMotion.Auxiliary.DenseCountable

A dense countable subset of a second-countable topological space #

source
noncomputable def denseCountable (T : Type u_1) [TopologicalSpace T] [SecondCountableTopology T] :
Set T

A countable dense subset of a second-countable topological space.

Equations
Instances For
    source
    theorem dense_denseCountable {T : Type u_1} [TopologicalSpace T] [SecondCountableTopology T] :
    Dense (denseCountable T)
    source
    theorem countable_denseCountable {T : Type u_1} [TopologicalSpace T] [SecondCountableTopology T] :
    (denseCountable T).Countable