instLEInftyOfNatWithTopENat_1

Mathlib.Geometry.Manifold.IsManifold.Basic

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

English

There is an instance LEInfty of 1 in WithTop ℕ∞.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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