coePNat

Mathlib.Data.PNat.Prime

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

English

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

Русский

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

LaTeX

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

Lean4

instance coePNat : Coe Nat.Primes ℕ+ :=
  ⟨toPNat⟩

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

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

Разделы

Аффилиация

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