coe_natGT

Mathlib.Order.OrderIsoNat

URI: https://scilib.ai/kg/mathlib#RelEmbedding.coe_natGT

English

The underlying function of natGT is f itself: the embedding's value equals f.

Русский

Базовая функция natGT равна f.

LaTeX

$$@[simp]\\theorem coe_natGT {f : ℕ → α} {H : ∀ n, r (f (n+1)) (f n)} : ⇑(natGT f H) = f$$

Lean4

@[simp]
theorem coe_natGT {f : ℕ → α} {H : ∀ n : ℕ, r (f (n + 1)) (f n)} : ⇑(natGT f H) = f :=
  rfl

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

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

Разделы

Аффилиация

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