coe_pnat_nat

Mathlib.Data.PNat.Prime

URI: https://scilib.ai/kg/mathlib#Nat.Primes.coe_pnat_nat

English

The image of Finset Ioo a b under the canonical embedding equals Finset Ioo a.val b.val.

Русский

Образ Finset Ioo a b при каноническом вложении равен Finset Ioo a.val b.val.

LaTeX

$$$(Ioo(a,b)).map(Embedding.subtype\\, _) = Ioo(a.{\\mathrm{val}}, b.{\\mathrm{val}})$$$

Lean4

@[norm_cast]
theorem coe_pnat_nat (p : Nat.Primes) : ((p : ℕ+) : ℕ) = p :=
  rfl

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

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

Разделы

Аффилиация

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