toPNat

Mathlib.Data.PNat.Prime

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

English

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

Русский

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

LaTeX

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

Lean4

/-- The canonical map from `Nat.Primes` to `ℕ+` -/
@[coe]
def toPNat : Nat.Primes → ℕ+ := fun p => ⟨(p : ℕ), p.property.pos⟩

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

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

Разделы

Аффилиация

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