map_subtype_embedding_Ioc — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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