preimage_cast_Ioi — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem preimage_cast_Ioi (q : ℚ) : (↑) ⁻¹' Ioi (q : K) = Ioi q :=
  castOrderEmbedding.preimage_Ioi q

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