image_sub_const_Icc — Mathlib

English

Let α be an ordered additive group. For any b ≤ c, the image of [b, c] under x ↦ a − x is [a − c, a − b].

Русский

Пусть α — упорядоченная аддитивная группа. Для любых b ≤ c образ [b, c] при отображении x ↦ a − x равен [a − c, a − b].

LaTeX

$$$ \{ a - x \mid x \in [b, c] \} = [a - c, a - b]$$$

Lean4

@[simp]
theorem image_sub_const_Icc : (fun x => x - a) '' Icc b c = Icc (b - a) (c - a) := by simp [sub_eq_neg_add]

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