English
Let p be a predicate on α and u a permutation of the subtype {a ∈ α | p a}. Then the support of the ambient extension of u equals the image of the subtype support under the subtype-embedding.
Русский
Пусть p — предикат на α, и u перестановка над подтипом {a ∈ α | p a}. Тогда опора расширения в α совпадает с отображением опоры подтипа через вложение подтипа.
LaTeX
$$$p:\alpha \to \text{Prop},\; u:\operatorname{Perm}(\operatorname{Subtype} p).\; (\operatorname{ofSubtype} u).\operatorname{support} = \operatorname{map}(\operatorname{Function.Embedding.subtype} p)\; u.\operatorname{support}$$$
Lean4
theorem support_ofSubtype {p : α → Prop} [DecidablePred p] (u : Perm (Subtype p)) :
(ofSubtype u).support = u.support.map (Function.Embedding.subtype p) :=
by
ext x
simp only [mem_support, ne_eq, Finset.mem_map, Function.Embedding.coe_subtype, Subtype.exists, exists_and_right,
exists_eq_right, not_iff_comm, not_exists, not_not]
by_cases hx : p x
· simp only [forall_prop_of_true hx, ofSubtype_apply_of_mem u hx, ← Subtype.coe_inj]
· simp only [forall_prop_of_false hx, ofSubtype_apply_of_not_mem u hx]
