coe_mem_cutMap_iff — Mathlib

English

For any rational q, cutMap β (q : α) equals the image of rationals below q under Rat.cast.

Русский

Для рационала q разрезная карта cutMap β (q : α) равна образу рационалов, меньших q, под Rat.cast.

LaTeX

$$$\operatorname{cutMap}_{β}(q : \alpha) = \operatorname{Rat.cast}''\{ r : \mathbb{Q} \mid (r : β) < q \}$$$

Lean4

theorem coe_mem_cutMap_iff [CharZero β] : (q : β) ∈ cutMap β a ↔ (q : α) < a :=
  Rat.cast_injective.mem_set_image

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