Ico_add_bij — Mathlib

English

The translation by d maps the half-open interval Ico(a, b) bijectively onto Ico(a + d, b + d).

Русский

Перенос на d переводит полузакрытый интервал Ico(a, b) в Ico(a + d, b + d) биективно.

LaTeX

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

Lean4

theorem Ico_add_bij : BijOn (· + d) (Ico a b) (Ico (a + d) (b + d)) :=
  by
  rw [← Ici_inter_Iio, ← Ici_inter_Iio]
  exact (Ici_add_bij a d).inter_mapsTo (fun x hx => add_lt_add_right hx _) fun x hx => lt_of_add_lt_add_right hx.2

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