map_subtype_embedding_Ico — Mathlib

English

The canonical embedding sends the PNats interval Ico a b to the Nat interval Ico a.val b.val.

Русский

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

LaTeX

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

Lean4

theorem map_subtype_embedding_Ico : (Ico a b).map (Embedding.subtype _) = Ico ↑a ↑b :=
  Finset.map_subtype_embedding_Ico _ _ _ fun _c _ _x hx _ hc _ => hc.trans_le hx

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