instLEInftyOfNatWithTopENat_2

Mathlib.Geometry.Manifold.IsManifold.Basic

URI: https://scilib.ai/kg/mathlib#IsManifold.instLEInftyOfNatWithTopENat_2

English

There is an instance LEInfty 0 for WithTop ℕ∞.

Русский

Существует LEInfty 0 для WithTop ℕ∞.

LaTeX

$$$(0 : WithTop ℕ∞) \text{ has LEInfty}$$$

Lean4

instance : LEInfty (0 : WithTop ℕ∞) :=
  inferInstanceAs (LEInfty ((0 : ℕ) : WithTop ℕ∞))

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

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

Разделы

Аффилиация

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