English
Let u be a permutation on the subtype and consider its extension; the supported elements in the ambient type correspond to those moved within the subtype, mapped via the embedding.
Русский
Пусть u — перестановка на подтипе, и рассмотрим её расширение; поддерживаемые элементы в окружности соответствуют тем, которые движутся внутри подтипа, отображаясь вложением.
LaTeX
$$$\operatorname{support}(\operatorname{ofSubtype} u) = \operatorname{map}(\operatorname{Embedding.subtype} p)\; u.\operatorname{support}$$$
Lean4
theorem support_prod_le (l : List (Perm α)) : l.prod.support ≤ (l.map support).foldr (· ⊔ ·) ⊥ := by
induction l with
| nil => simp
| cons hd tl hl =>
rw [List.prod_cons, List.map_cons, List.foldr_cons]
refine (support_mul_le hd tl.prod).trans ?_
exact sup_le_sup le_rfl hl
