cast_le_ofNat — Mathlib

English

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

Русский

Пусть p ∈ ℚ≥0 и n ∈ ℕ, причём n ≥ 2. Тогда (p : K) ≤ ofNat(n) в K эквивалентно p ≤ OfNat.ofNat n в ℚ≥0.

LaTeX

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

Lean4

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

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