depth_pos

Mathlib.Data.W.Basic

URI: https://scilib.ai/kg/mathlib#WType.depth_pos

English

Every nonempty W-type term has positive depth: 0 < t.depth.

Русский

Любой элемент WType имеет положительную глубину: 0 < t.depth.

LaTeX

$$$\forall t:\, WType(β),\ 0 < t.depth.$$$

Lean4

theorem depth_pos (t : WType β) : 0 < t.depth := by
  cases t
  apply Nat.succ_pos

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

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

Разделы

Аффилиация

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