preimage_div_const_uIcc

Mathlib.Algebra.Order.Group.Pointwise.Interval

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

← MathLib Explorer

English

For a ≠ 0, the preimage of [[b, c]] under x ↦ x/a equals [[b a, c a]].

Русский

Если a ≠ 0, то предобраз от [[b, c]] по x/a равен [[b a, c a]].

LaTeX

$$$\{ x \in \alpha : \frac{x}{a} \in [[b, c]] \} = [[b a, c a]]$$

Lean4

@[simp]
theorem preimage_div_const_uIcc (ha : a ≠ 0) (b c : α) : (fun x => x / a) ⁻¹' [[b, c]] = [[b * a, c * a]] := by
  simp only [div_eq_mul_inv, preimage_mul_const_uIcc (inv_ne_zero ha), inv_inv]

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

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

Разделы

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

Аффилиация

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