map_subtype_embedding_Ioo — Mathlib

English

If hp holds, mapping Embedding.subtype p on Ioo a b equals Ioo a.val b.val: (Ioo a b).map Embedding.subtype p = (Ioo a.val b.val).

Русский

При выполнении условия hp отображение Embedding.subtype p на Ioo a b даёт Ioo a.val b.val.

LaTeX

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

Lean4

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

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