Ico_image_const_sub_eq_Ico — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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