preimage_mul_const_uIcc — Mathlib

English

For a nonzero a and any b, c, the preimage of the closed-union interval [[b, c]] under x ↦ x·a is the closed-union interval [[b/a, c/a]].

Русский

Для непустого канонического множителя a ≠ 0 и любых b, c, предобраз под x ↦ x·a замыкается в [[b/a, c/a]].

LaTeX

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

Lean4

@[simp]
theorem preimage_mul_const_uIcc (ha : a ≠ 0) (b c : α) : (· * a) ⁻¹' [[b, c]] = [[b / a, c / a]] :=
  (lt_or_gt_of_ne ha).elim
    (fun h => by simp [← Icc_min_max, h, h.le, min_div_div_right_of_nonpos, max_div_div_right_of_nonpos])
    fun ha : 0 < a => by simp [← Icc_min_max, ha, ha.le, min_div_div_right, max_div_div_right]

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