conjneg_nonneg — Mathlib

English

For any function f from a group to a ordered star-ring, the nonnegativity of conjneg f is equivalent to the nonnegativity of f.

Русский

Для любой функции f: G → R в частично упорядоченной звездокольцу conjneg сохраняет неотрицательность, то есть 0 ≤ conjneg f эквивалентно 0 ≤ f.

LaTeX

$$$$ 0 \le \operatorname{conjneg} f \iff 0 \le f $$$$

Lean4

@[simp]
theorem conjneg_nonneg : 0 ≤ conjneg f ↔ 0 ≤ f :=
  (Equiv.neg _).forall_congr' <| by simp [starRingEnd_apply]

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