le_lift_iff — Mathlib

English

Let x ∈ ℕ and n ∈ ℕ∞ with h a witness that n < ⊤. Then x ≤ lift n h if and only if x ≤ n.

Русский

Пусть x ∈ ℕ и n ∈ ℕ∞, и h — доказательство того, что n < ⊤. Тогда x ≤ lift n h тогда же x ≤ n.

LaTeX

$$$\\\\forall x \\\\in \\\\mathbb{N}, \\\\forall n \\\\in \\\\mathbb{N}_{\\\\infty}, \\\\forall h \ (h \\\\colon n < \\\\top),\\\\ x \\\\le \\\\operatorname{lift}(n,h) \\\\\\\iff \\\\ x \\\\le n.$$$

Lean4

@[simp]
theorem le_lift_iff {x : ℕ} {n : ℕ∞} {h} : x ≤ lift n h ↔ x ≤ n :=
  WithTop.le_untop_iff _

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