Ioc_add_bij — Mathlib

English

Under the same assumptions, translating by d gives a bijection from Ioc(a, b) to Ioc(a + d, b + d).

Русский

При тех же предположениях перенос на d задаёт биекцию между Ioc(a, b) и Ioc(a + d, b + d).

LaTeX

$$$Ioc(a,b) + d = Ioc(a+d,b+d)$$$

Lean4

theorem Ioc_add_bij : BijOn (· + d) (Ioc a b) (Ioc (a + d) (b + d)) :=
  by
  rw [← Ioi_inter_Iic, ← Ioi_inter_Iic]
  exact (Ioi_add_bij a d).inter_mapsTo (fun x hx => add_le_add_right hx _) fun x hx => le_of_add_le_add_right hx.2

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