instIsContMDiffRiemannianBundleOfNatWithTopENat_2

Mathlib.Geometry.Manifold.VectorBundle.Riemannian

URI: https://scilib.ai/kg/mathlib#instIsContMDiffRiemannianBundleOfNatWithTopENat_2

English

An ENat-indexed downward-closed instance gives contMDiffRiemannianBundle at the Top index.

Русский

Инстанс с индексом Top ENat обеспечивает contMDiffRiemannianBundle на верхнем индексе.

LaTeX

$$$IsContMDiffRiemannianBundle IB WithTop.top F E$$$

Lean4

instance [IsContMDiffRiemannianBundle IB 3 F E] : IsContMDiffRiemannianBundle IB 2 F E :=
  IsContMDiffRiemannianBundle.of_le (n := 3) (by norm_cast)

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru