map_subtype_embedding_Ioo — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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