Chosen countable dense subset

Definition

KLSModular_BrownianMotion_Auxiliary_DenseCountable

by Lazyfill · Oct 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-contextvendored-brownianmotion

Vendored from RemyDegenne/brownian-motion at commit a7ad7af662044313bc80a7c0756360fb3745f931 under Apache-2.0. For a second-countable topological space T, denseCountable T is a chosen countable dense subset, with dense_denseCountable and countable_denseCountable recording its density and countability.

Original module imports

public import Mathlib.Topology.Bases

Original declaration excerpt

Shown in the original module context.

def denseCountable (T : Type*) [TopologicalSpace T] [SecondCountableTopology T] : Set T :=
  (TopologicalSpace.exists_countable_dense T).choose

Module navigation

Project result: The KLS conjecture.

Original module · BrownianMotion.Auxiliary.DenseCountable · Frozen source 408915f.

Definition code

import Mathlib.Topology.Bases

/-
Copyright (c) 2026 Rémy Degenne. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rémy Degenne
-/
-- Vendored from https://github.com/RemyDegenne/brownian-motion at commit a7ad7af662044313bc80a7c0756360fb3745f931 (upstream path BrownianMotion/Auxiliary/DenseCountable.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
section
/-- A countable dense subset of a second-countable topological space. -/
def denseCountable (T : Type*) [TopologicalSpace T] [SecondCountableTopology T] : Set T :=
  (TopologicalSpace.exists_countable_dense T).choose
lemma dense_denseCountable {T : Type*} [TopologicalSpace T] [SecondCountableTopology T] :
    Dense (denseCountable T) :=
  (TopologicalSpace.exists_countable_dense T).choose_spec.2
lemma countable_denseCountable {T : Type*} [TopologicalSpace T] [SecondCountableTopology T] :
    (denseCountable T).Countable :=
  (TopologicalSpace.exists_countable_dense T).choose_spec.1

Source

Lean source: https://github.com/RemyDegenne/brownian-motion/blob/a7ad7af662044313bc80a7c0756360fb3745f931/BrownianMotion/Auxiliary/DenseCountable.lean#L17-L27 (repository human-ai-mathematics/kls-lean, commit 408915f, module `BrownianMotion.Auxiliary.DenseCountable`, definition bundle `KLSModular_BrownianMotion_Auxiliary_DenseCountable`; the repository is private at upload time). Vendored from https://github.com/RemyDegenne/brownian-motion at commit a7ad7af662044313bc80a7c0756360fb3745f931 (Apache-2.0; upstream copyright notice retained in the Lean text).

View graph