map_subtype_embedding_Ioc — Mathlib

English

If hp ensures p is preserved for a ≤ x ≤ b, then mapping Embedding.subtype p on Ioc a b equals Ioc a.val b.val: (Ioc a b).map Embedding.subtype p = (Ioc a.val b.val).

Русский

Если hp сохраняет p при a ≤ x ≤ b, отображение Embedding.subtype p на Ioc a b даёт Ioc a.val b.val.

LaTeX

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

Lean4

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

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