preimage_cast_uIcc — Mathlib

English

For p, q ∈ ℚ, the preimage of the closed interval under the cast embedding preserves the uIcc interval: Set.preimage cast (Set.uIcc p.cast q.cast) = Set.uIcc p q.

Русский

Для p, q ∈ ℚ обеспечивается сохранение интервала uIcc через приведение: предобразование равняется uIcc(p,q) в ℚ.

LaTeX

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

Lean4

@[simp]
theorem preimage_cast_uIcc (p q : ℚ) : (↑) ⁻¹' uIcc (p : K) q = uIcc p q :=
  (castOrderEmbedding (K := K)).preimage_uIcc p q

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