Ioo_add_bij — Mathlib

English

Let M be an ordered cancellative additively commutative monoid. Then translating by d carries the open interval Ioo(a, b) bijectively onto Ioo(a + d, b + d).

Русский

Пусть M — упорядоченная коммутативная по сложению моноида; перенос на d отображает открытый интервал Ioo(a, b) биекцией на Ioo(a + d, b + d).

LaTeX

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

Lean4

theorem Ioo_add_bij : BijOn (· + d) (Ioo a b) (Ioo (a + d) (b + d)) :=
  by
  rw [← Ioi_inter_Iio, ← Ioi_inter_Iio]
  exact (Ioi_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

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