image_neg_Iic — Mathlib

English

Let α be an ordered additive group. The image of Iic a under negation is Ici(−a); i.e. { x ≤ a } mapped by x ↦ −x equals { y ≥ −a }.

Русский

Пусть α — упорядоченная аддитивная группа. Образ Iic a при применении отрицания равен Ici(−a); то есть { x ≤ a } переходит в { y ≥ −a }.

LaTeX

$$$$\\{ x \\le a \\} \\mapsto -x \\in \\alpha \\Rightarrow \\{ y \\ge -a \\}$$$$

Lean4

theorem image_neg_Iic : Neg.neg '' Iic a = Ici (-a) := by simp

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