map_subtype_embedding_uIcc — Mathlib

English

The canonical embedding carries the PNats interval uIcc a b to the Nat interval uIcc a.val b.val.

Русский

Каноническое вложение переводит PNats‑интервал uIcc a b в Nat‑интервал uIcc a.val b.val.

LaTeX

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

Lean4

theorem map_subtype_embedding_uIcc : (uIcc a b).map (Embedding.subtype _) = uIcc ↑a ↑b :=
  map_subtype_embedding_Icc _ _

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