ofNat_le_cast — Mathlib

English

For p ∈ ℚ≥0 and n ∈ ℕ with n ≥ 2, ofNat(n) ≤ (p : K) in K is equivalent to OfNat.ofNat n ≤ p in ℚ≥0.

Русский

Для p ∈ ℚ≥0 и n ∈ ℕ (n ≥ 2) неравенство ofNat(n) ≤ p в K эквивалентно OfNat.ofNat n ≤ p в ℚ≥0.

LaTeX

$$$\operatorname{ofNat}(n) \le (p : K) \iff \operatorname{OfNat}.ofNat(n) \le p$$$

Lean4

@[simp]
theorem ofNat_le_cast : ofNat(n) ≤ (p : K) ↔ OfNat.ofNat n ≤ p := by simp [← cast_le (K := K)]

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