val_eq_cast

Mathlib.Data.NNRat.Defs

URI: https://scilib.ai/kg/mathlib#NNRat.val_eq_cast

English

For any q ∈ ℚ≥0, the underlying rational equals the first component of the pair, i.e., q.1 = q.

Русский

Для любого q ∈ ℚ≥0, раннее рациональное число совпадает с первым компонентом пары: q.1 = q.

LaTeX

$$$\forall q \in \mathbb{Q}_{\ge 0},\ q.1 = q$$$

Lean4

@[simp]
theorem val_eq_cast (q : ℚ≥0) : q.1 = q :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru