preimage_cast_Icc — Mathlib

English

For p, q ∈ ℚ, the preimage under the cast map of the closed interval [p, q] in K is exactly the closed interval [p, q] in ℚ: Set.preimage cast (Icc p.cast q.cast) = Icc p q.

Русский

Пусть p, q ∈ ℚ. Образ обратной проекции отображения приведения от K к ℚ закрытого отрезка [p, q] совпадает с отрезком [p, q] в ℚ.

LaTeX

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

Lean4

@[simp]
theorem preimage_cast_Icc (p q : ℚ) : (↑) ⁻¹' Icc (p : K) q = Icc p q :=
  castOrderEmbedding.preimage_Icc ..

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