image_const_sub_uIcc — Mathlib

English

Let a,b,c,d be elements of an ordered additive group. Then the image of the closed interval [b,c] under the map x ↦ a − x is the closed interval [a − b, a − c].

Русский

Пусть a, b, c, d — элементы упорядоченной аддитивной группы. Образ единичного интервала [b, c] под отображением x ↦ a − x есть интервал [a − b, a − c].

LaTeX

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

Lean4

@[simp]
theorem image_const_sub_uIcc : (fun x => a - x) '' [[b, c]] = [[a - b, a - c]] :=
  by
  have := image_comp (fun x => a + x) fun x => -x; dsimp [Function.comp_def] at this
  simp [sub_eq_add_neg, this, add_comm]

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