image_neg_Ici — Mathlib

English

Let α be an ordered additive group. The image of Ici a under negation is Iic(−a); i.e. { x ∈ α | x ≥ a } mapped by x ↦ −x equals { y ∈ α | y ≤ −a }.

Русский

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

LaTeX

$$$$\\{ x \\in \\alpha \\mid x \\ge a \\} \\mapsto -x \\in \\alpha \\;\\Rightarrow\\; \\{ y \\in \\alpha \\mid y \\le -a \\}$$$$

Lean4

theorem image_neg_Ici : Neg.neg '' Ici a = Iic (-a) := by simp

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