instLEInftyCastWithTopENat

Mathlib.Geometry.Manifold.IsManifold.Basic

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

English

For any n ≥ 2, there is an LEInfty instance corresponding to OfNat n in WithTop ℕ∞.

Русский

Для любого n ≥ 2 существует LEInfty-инстанс для OfNat n в WithTop ℕ∞.

LaTeX

$$$(n: Nat) [n.AtLeastTwo] : ENat.LEInfty (OfNat.ofNat n)$$$

Lean4

instance (n : ℕ) : LEInfty (n : WithTop ℕ∞) :=
  ⟨mod_cast le_top⟩

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

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

Разделы

Аффилиация

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