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