preimage_cast_Ici — Mathlib

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

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