map_subtype_embedding_Ico — Mathlib

English

If hp ensures p is preserved along the interval, then mapping Embedding.subtype p on Ico a b yields Ico a.val b.val: (Ico a b).map Embedding.subtype p = (Ico a.val b.val).

Русский

При условии, что p сохраняется по интервалу, отображение Embedding.subtype p на Ico a b даёт Ico a.val b.val.

LaTeX

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

Lean4

theorem map_subtype_embedding_Ico (hp : ∀ ⦃a b x⦄, a ≤ x → x ≤ b → p a → p b → p x) :
    (Ico a b).map (Embedding.subtype p) = (Ico a b : Finset α) :=
  by
  rw [subtype_Ico_eq]
  refine Finset.subtype_map_of_mem fun x hx => ?_
  rw [mem_Ico] at hx
  exact hp hx.1 hx.2.le a.prop b.prop

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