Iic_add_bij

Mathlib.Algebra.Order.Group.Pointwise.Interval

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

English

The map x ↦ x + a induces a bijection from Iic b to Iic (b + a).

Русский

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

LaTeX

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

Lean4

theorem Iic_add_bij : BijOn (· + a) (Iic b) (Iic (b + a)) :=
  image_add_const_Iic a b ▸ (add_left_injective _).injOn.bijOn_image

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

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

Разделы

Аффилиация

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