Theorem IsContMDiffRiemannianBundle.of_le

Modification history

2025-07-04 20:03
Mathlib/Geometry/Manifold/VectorBundle/Riemannian.lean
feat: smooth Riemannian bundles (#26506) …
Added IsContMDiffRiemannianBundle.of_leView on Github →