image_neg_Ioo — Mathlib

English

Let α be an ordered additive group. The image of Ioo a b under negation is Ioo(−b, −a); i.e. { x ∈ α : a < x < b } mapped by x ↦ −x equals { y ∈ α : −b < y < −a }.

Русский

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

LaTeX

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

Lean4

theorem image_neg_Ioo : Neg.neg '' Ioo a b = Ioo (-b) (-a) := by simp

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