sq_le_one_iff₀

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

URI: https://scilib.ai/kg/mathlib#sq_le_one_iff₀

English

If a ≥ 0, then a^2 ≤ 1 iff a ≤ 1.

Русский

Если a ≥ 0, то a^2 ≤ 1 тогда и только тогда, когда a ≤ 1.

LaTeX

$$$0 \le a \Rightarrow a^2 \le 1 \iff a \le 1$$$

Lean4

theorem sq_le_one_iff₀ (ha : 0 ≤ a) : a ^ 2 ≤ 1 ↔ a ≤ 1 :=
  pow_le_one_iff_of_nonneg ha (Nat.succ_ne_zero _)

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

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

Разделы

Аффилиация

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