preimage_const_mul_Ioi_of_neg — Mathlib

English

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

Русский

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

LaTeX

$$$\{ x \in \alpha \mid c x > a \} = \left( -\infty, \frac{a}{c} \right)$$$

Lean4

@[simp]
theorem preimage_const_mul_Ioi_of_neg (a : α) {c : α} (h : c < 0) : (c * ·) ⁻¹' Ioi a = Iio (a / c) := by
  simpa only [mul_comm] using preimage_mul_const_Ioi_of_neg a h

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