image_neg_Icc — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem image_neg_Icc : Neg.neg '' Icc a b = Icc (-b) (-a) := by simp

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