OAI/GroupTheory/PolycyclicRecognition/Algebra/NilpotentChartCountability.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Countability and Haar measure on the chosen nilpotent factors

  1. theorem OAI.PolycyclicRecognition.NilpotentLieModel.secondCountable_of_chart line 17

    Source documentation

    The actual exponential chart transports the countable topology of a finite-dimensional real vector space to the selected factor.

    theorem secondCountable_of_chart
    (chart : GroupLieAlgebra (𝓘(ℝ, N.modelSpace)) N.carrier ≃ₜ N.carrier) :
    SecondCountableTopology N.carrier := by
…