Iio_add_bij

Mathlib.Algebra.Order.Group.Pointwise.Interval

URI: https://scilib.ai/kg/mathlib#Set.Iio_add_bij

English

The map x ↦ x + a is a bijection from Iio b to Iio (b + a).

Русский

Отображение x ↦ x + a задаёт биекцию от Iio b к Iio (b + a).

LaTeX

$$BijOn (λ x, x + a) (Iio b) (Iio (b + a))$$

Lean4

theorem Iio_add_bij : BijOn (· + a) (Iio b) (Iio (b + a)) :=
  image_add_const_Iio a b ▸ (add_left_injective _).injOn.bijOn_image

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru