ofReal_nnratCast — Mathlib

English

Let K be a type with a real-to-K embedding. For every q in the nonnegative rationals ℚ≥0, the image of q under the real-to-K embedding equals q in K.

Русский

Пусть K — тип с отображением вещественных чисел в K. Для любого q ∈ ℚ≥0 образ q через вещественное вложение в K совпадает с самим элементом q в K.

LaTeX

$$$$\forall q \in \mathbb{Q}_{\ge 0},\ ((q : \mathbb{R}) : K) = q. $$$$

Lean4

@[rclike_simps, norm_cast]
theorem ofReal_nnratCast (q : ℚ≥0) : ((q : ℝ) : K) = q :=
  map_nnratCast (algebraMap ℝ K) _

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