Icc_add_bij

Mathlib.Algebra.Order.Interval.Set.Monoid

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

← MathLib Explorer

English

Ioo(0,1) is closed under multiplication.

Русский

Ioo(0,1) замкнуто относительно умножения.

LaTeX

$$$\forall p,q \in (0,1),\ 0 < p q < 1$$$

Lean4

theorem Icc_add_bij : BijOn (· + d) (Icc a b) (Icc (a + d) (b + d)) :=
  by
  rw [← Ici_inter_Iic, ← Ici_inter_Iic]
  exact (Ici_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

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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