English
Assume hp ensures p is closed under the interval: a ≤ x ≤ b implies p a, p b, p x. Then mapping Embedding.subtype p on Icc a b yields the α-interval Icc a.val b.val: (Icc a b).map Embedding.subtype p = (Icc a.val b.val).
Русский
Пусть hp обеспечивает замкнутость p относительно интервала: a ≤ x ≤ b влечёт p a, p b, p x. Тогда отображение Embedding.subtype p на Icc a b даёт α-интервал: (Icc a b).map Embedding.subtype p = Icc a.val b.val.
LaTeX
$$$$ (\\mathrm{Icc}(a,b)).\\mathrm{map}(\\mathrm{Embedding.subtype}\\ p) = \\mathrm{Icc}(a.\\mathrm{val}, b.\\mathrm{val}). $$$$
Lean4
theorem map_subtype_embedding_Icc (hp : ∀ ⦃a b x⦄, a ≤ x → x ≤ b → p a → p b → p x) :
(Icc a b).map (Embedding.subtype p) = (Icc a b : Finset α) :=
by
rw [subtype_Icc_eq]
refine Finset.subtype_map_of_mem fun x hx => ?_
rw [mem_Icc] at hx
exact hp hx.1 hx.2 a.prop b.prop
