cutMap_coe — Mathlib

English

Alternative expression for cutMap with coe; cutMap β (q : α) equals Rat.cast image of rationals below q.

Русский

Альтернативное выражение cutMap через внедрение; cutMap β (q : α) равно образу Rat.cast рационалов ниже q.

LaTeX

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

Lean4

theorem cutMap_coe (q : ℚ) : cutMap β (q : α) = Rat.cast '' {r : ℚ | (r : β) < q} := by simp_rw [cutMap, Rat.cast_lt]

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