image_sub_const_Ico — 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_Ico : (fun x => x - a) '' Ico b c = Ico (b - a) (c - a) := by simp [sub_eq_neg_add]

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