lt_lift_iff

Mathlib.Data.ENat.Basic

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

English

For x ∈ ℕ and n ∈ ENNat with an appropriate bound, x < lift(n,h) iff x < n.

Русский

Для x ∈ ℕ и n ∈ ENat с подходящим ограничением, x < lift(n,h) ⇔ x < n.

LaTeX

$$$$ x < \\operatorname{lift}(n,h) \\iff x < n. $$$$

Lean4

@[simp]
theorem lt_lift_iff {x : ℕ} {n : ℕ∞} {h} : x < lift n h ↔ x < n :=
  WithTop.lt_untop_iff _

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

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

Разделы

Аффилиация

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