powerlt_zero

Mathlib.SetTheory.Cardinal.Basic

URI: https://scilib.ai/kg/mathlib#Cardinal.powerlt_zero

← MathLib Explorer

English

For any a, a^{<0} = 0.

Русский

Для любого a: a^{<0} = 0.

LaTeX

$$$a^{<0} = 0$$$

Lean4

@[simp]
theorem powerlt_zero {a : Cardinal} : a ^< 0 = 0 :=
  by
  convert Cardinal.iSup_of_empty _
  exact Subtype.isEmpty_of_false fun x => mem_Iio.not.mpr (Cardinal.zero_le x).not_gt

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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