image_neg_Ioi — Mathlib

English

Let α be an ordered additive group. The image of Ioi a under negation is Iio(−a); i.e. { x > a } mapped by x ↦ −x equals { y < −a }.

Русский

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

LaTeX

$$$$\\{ x \\mid x > a \\} \\mapsto -x ∈ \\alpha \\Rightarrow \\{ y \\mid y < -a \\}$$$$

Lean4

theorem image_neg_Ioi : Neg.neg '' Ioi a = Iio (-a) := by simp

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