preimage_cast_Ico — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem preimage_cast_Ico (p q : ℚ) : (↑) ⁻¹' Ico (p : K) q = Ico p q :=
  castOrderEmbedding.preimage_Ico ..

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