instIsContMDiffRiemannianBundleOfNatWithTopENat

Mathlib.Geometry.Manifold.VectorBundle.Riemannian

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

English

A top-level ENat-based instance lifts contMDiffRiemannianBundle to Top-space.

Русский

Инстанс сверху по ENat поднимает contMDiffRiemannianBundle в верхнее пространство.

LaTeX

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

Lean4

instance [IsContMDiffRiemannianBundle IB 1 F E] : IsContMDiffRiemannianBundle IB 0 F E :=
  IsContMDiffRiemannianBundle.of_le zero_le_one

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

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

Разделы

Аффилиация

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