OAI/Geometry/RCD/Sobolev/FiniteSpanOfIndependentBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite dimension from a bound on independent generators

  1. theorem OAI.RegularPointCoordinates.finite_span_of_independent_bound line 15