preimage_cast_Icc — Mathlib

English

The preimage under cast of the closed interval Icc(p,q) is exactly the closed interval Icc(p,q) in ℚ≥0.

Русский

Обратное образование под отображением cast от Icc(p,q) даёт точно Icc(p,q) в ℚ≥0.

LaTeX

$$$\operatorname{preimage} \bigl(\text{cast}, [p,q]_{K}\bigr) = [p,q]_{\mathbb{Q}_{\ge 0}}$$$

Lean4

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

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