preimage_cast_Iio — Mathlib

English

For q ∈ ℚ, the preimage of the open ray (−∞, q) under cast equals (−∞, q) in ℚ: Set.preimage cast (Set.Iio q.cast) = Set.Iio q.

Русский

Пусть q ∈ ℚ. Обратная образующая для луча (−∞, q) сохраняется через приведение: предобразование равно (−∞, q) в ℚ.

LaTeX

$$$\operatorname{Set.preimage}(\operatorname{cast}, \operatorname{Iio}(q.cast)) = \operatorname{Iio}(q)$$$

Lean4

@[simp]
theorem preimage_cast_Iio (q : ℚ) : (↑) ⁻¹' Iio (q : K) = Iio q :=
  castOrderEmbedding.preimage_Iio q

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