preimage_cast_Iic — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem preimage_cast_Iic (q : ℚ) : (↑) ⁻¹' Iic (q : K) = Iic q :=
  castOrderEmbedding.preimage_Iic q

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