cast_nonpos

Mathlib.Data.Rat.Cast.Order

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

English

For q ∈ ℚ≥0, (q.cast ≤ 0) is equivalent to (q ≤ 0).

Русский

Для q ∈ ℚ≥0 верно: q.cast ≤ 0 тогда и только тогда, когда q ≤ 0.

LaTeX

$$$(q : K) \le 0 \leftrightarrow q \le 0$$$

Lean4

@[simp]
theorem cast_nonpos : (q : K) ≤ 0 ↔ q ≤ 0 := by norm_cast

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

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

Разделы

Аффилиация

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