intCast_le_cast

Mathlib.Data.Rat.Cast.Order

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

English

For m ∈ ℤ and n ∈ ℚ, m.cast ≤ n.cast iff m ≤ n.cast.

Русский

Для m ∈ ℤ и n ∈ ℚ, m.cast ≤ n.cast эквивалентно m ≤ n.cast.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem intCast_le_cast {m : ℤ} {n : ℚ} : (m : K) ≤ n ↔ (m : ℚ) ≤ n := by rw [← cast_le (K := K), cast_intCast]

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

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

Разделы

Аффилиация

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