addLECancellable_coe

Mathlib.Data.ENat.Basic

URI: https://scilib.ai/kg/mathlib#ENat.addLECancellable_coe

English

For any natural a, AddLECancellable (a : ENat) holds.

Русский

Для любого натурального a выполняется AddLECancellable (a : ENat).

LaTeX

$$$\text{AddLECancellable}(a : ENat)$$$

Lean4

theorem addLECancellable_coe (a : ℕ) : AddLECancellable (a : ℕ∞) :=
  WithTop.addLECancellable_coe _

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

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

Разделы

Аффилиация

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