image_sub_const_Ico — Mathlib

English

If c ≤ a, the image of Ico(a,b) under x ↦ x − c is Ico(a−c, b−c).

Русский

Пусть c ≤ a. Образ Ico(a,b) при x ↦ x−c равен Ico(a−c, b−c).

LaTeX

$$$(Ico(a,b)).image (\\lambda x, x - c) = Ico(a - c, b - c)$$$

Lean4

theorem image_sub_const_Ico (h : c ≤ a) : ((Ico a b).image fun x => x - c) = Ico (a - c) (b - c) :=
  by
  ext x
  simp_rw [mem_image, mem_Ico]
  refine ⟨?_, fun h ↦ ⟨x + c, by cutsat⟩⟩
  rintro ⟨x, hx, rfl⟩
  cutsat

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