mk_nnratCast

Mathlib.Algebra.Order.Nonneg.Field

URI: https://scilib.ai/kg/mathlib#Nonneg.mk_nnratCast

English

The embedding of q.cast into the nonnegative subtype equals its cast; i.e., ⟨q.cast, q.cast_nonneg⟩ = q.cast.

Русский

Встройка q.cast в подпредмет неотрицательных элементов равна q.cast.

LaTeX

$$$\\langle q.cast, q.cast\\_nonneg \\rangle = q.cast$$$

Lean4

@[simp]
theorem mk_nnratCast (q : ℚ≥0) : (⟨q, q.cast_nonneg⟩ : { x : α // 0 ≤ x }) = q :=
  rfl

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

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

Разделы

Аффилиация

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