preimage_mul_const_Ici_of_neg

Mathlib.Algebra.Order.Group.Pointwise.Interval

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

← MathLib Explorer

English

For c < 0, the preimage of Ici(a) under x ↦ x c is Iic(a/c).

Русский

Для c < 0 предобраз Ici(a) по отображению x ↦ x c равен Iic(a/c).

LaTeX

$$$ (x \mapsto x c)^{-1} Ici(a) = Iic(a/c) $$$

Lean4

@[simp]
theorem preimage_mul_const_Ici_of_neg (a : α) {c : α} (h : c < 0) : (fun x => x * c) ⁻¹' Ici a = Iic (a / c) :=
  ext fun _x => (le_div_iff_of_neg h).symm

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

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

Разделы

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

Аффилиация

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