image_neg_Iio — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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