conjneg_neg'

Mathlib.Algebra.Order.Star.Conjneg

URI: https://scilib.ai/kg/mathlib#conjneg_neg'

English

Conjneg is an order-reversing involution on function space: conjneg f < 0 iff f < 0.

Русский

conjneg обращает порядок и инволютивно действует на пространство функций: conjneg f < 0 ⇔ f < 0.

LaTeX

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

Lean4

@[simp]
theorem conjneg_neg' : conjneg f < 0 ↔ f < 0 := by simp_rw [← neg_pos, ← conjneg_neg, conjneg_pos]

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

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

Разделы

Аффилиация

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