sqrt_nonneg

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

URI: https://scilib.ai/kg/mathlib#CFC.sqrt_nonneg

English

For every element a in the algebra, the square root is nonnegative: sqrt(a) ≥ 0.

Русский

Для любого элемента a в алгебре корень из a неотрицателен: sqrt(a) ≥ 0.

LaTeX

$$$0 \\leq \\sqrt{a}$$$

Lean4

@[simp, grind]
theorem sqrt_nonneg (a : A) : 0 ≤ sqrt a :=
  cfcₙ_predicate _ a

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

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

Разделы

Аффилиация

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