preimage_cast_uIoc — Mathlib

English

For p, q ∈ ℚ, the preimage of the half-open interval under cast equals the same interval in ℚ: Set.preimage cast (Set.uIoc p.cast q.cast) = Set.uIoc p q.

Русский

Для p, q ∈ ℚ предобразование полухваткого интервала через приведение даёт тот же интервал в ℚ.

LaTeX

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

Lean4

@[simp]
theorem preimage_cast_uIoc (p q : ℚ) : (↑) ⁻¹' uIoc (p : K) q = uIoc p q :=
  (castOrderEmbedding (K := K)).preimage_uIoc p q

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