cast_le_natCast

Mathlib.Data.Rat.Cast.Order

URI: https://scilib.ai/kg/mathlib#Rat.cast_le_natCast

English

For m ∈ ℚ and n ∈ ℕ, (m : K) ≤ n iff m ≤ n in ℚ.

Русский

Для m ∈ ℚ и n ∈ ℕ, (m : K) ≤ n тогда и только тогда, когда m ≤ n в ℚ.

LaTeX

$$$ \forall {m : \mathbb{Q}} {n : \mathbb{N}}, \ (m : K) \le n \leftrightarrow m \le (n : \mathbb{Q}). $$$

Lean4

@[simp, norm_cast]
theorem cast_le_natCast {m : ℚ} {n : ℕ} : (m : K) ≤ n ↔ m ≤ (n : ℚ) := by rw [← cast_le (K := K), cast_natCast]

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

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

Разделы

Аффилиация

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