natCast_lt_cast

Mathlib.Data.Rat.Cast.Order

URI: https://scilib.ai/kg/mathlib#NNRat.natCast_lt_cast

English

For m ∈ ℕ and n ∈ ℚ≥0, the inequality m < n.cast in K is equivalent to m < n in ℚ≥0.

Русский

Для m ∈ ℕ и n ∈ ℚ≥0: m < n.cast в K эквивалентно m < n в ℚ≥0.

LaTeX

$$$m < (n : K) \iff m < n$$$

Lean4

@[simp, norm_cast]
theorem natCast_lt_cast {m : ℕ} {n : ℚ≥0} : (m : K) < n ↔ (m : ℚ≥0) < n := by rw [← cast_lt (K := K), cast_natCast]

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

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

Разделы

Аффилиация

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