English
For q ∈ ℚ, the preimage of the closed ray [q, ∞) under cast equals [q, ∞) in ℚ: Set.preimage cast (Set.Ici q.cast) = Set.Ici q.
Русский
Пусть q ∈ ℚ. Образ обратной образующей отображения приведения от K к ℚ полунеотрезка [q, ∞) совпадает с [q, ∞) в ℚ.
LaTeX
$$$\operatorname{Set.preimage}(\operatorname{cast}, \operatorname{Ici}(q.cast)) = \operatorname{Ici}(q)$$$
Lean4
@[simp]
theorem preimage_cast_Ici (q : ℚ) : (↑) ⁻¹' Ici (q : K) = Ici q :=
castOrderEmbedding.preimage_Ici q