preimage_const_mul_Ico_of_neg — Mathlib

English

Let α be a field with a linear order and IsStrictOrderedRing. If c < 0 and a < b, then the preimage of the half-open interval [a, b) under x ↦ c·x is the half-open interval (b/c, a/c].

Русский

Пусть α — поле с линейным порядком и IsStrictOrderedRing. При c < 0 и a < b имеем: { x ∈ α : a ≤ x c < b } = (b/c, a/c].

LaTeX

$$$\{ x \in \alpha \mid a \le x c < b \} = \left( \frac{b}{c}, \frac{a}{c} \right]$$$

Lean4

@[simp]
theorem preimage_const_mul_Ico_of_neg (a b : α) {c : α} (h : c < 0) : (c * ·) ⁻¹' Ico a b = Ioc (b / c) (a / c) := by
  simpa only [mul_comm] using preimage_mul_const_Ico_of_neg a b h

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