image_neg_Ico — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem image_neg_Ico : Neg.neg '' Ico a b = Ioc (-b) (-a) := by simp

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