English
For a subtype extension u ∈ Perm(Subtype p), the support of the ambient extension equals the map of u.support under the subtype-embedding.
Русский
Для расширения v из Perm(Subtype p) выражение opорa в окружности α равна отображению опоры u через вложение подтипа.
LaTeX
$$$\operatorname{supp}(\operatorname{ofSubtype} u) = \operatorname{map}(\operatorname{Function.Embedding.subtype} p)\; u.\operatorname{support}$$$
Lean4
theorem support_noncommProd {ι : Type*} {k : ι → Perm α} {s : Finset ι}
(hs : Set.Pairwise s fun i j ↦ Disjoint (k i) (k j)) :
(s.noncommProd k (hs.imp (fun _ _ ↦ Perm.Disjoint.commute))).support = s.biUnion fun i ↦ (k i).support := by
classical
induction s using Finset.induction_on with
| empty => simp
| insert i s hi
hrec =>
have hs' : (s : Set ι).Pairwise fun i j ↦ Disjoint (k i) (k j) :=
hs.mono (by simp only [Finset.coe_insert, Set.subset_insert])
rw [Finset.noncommProd_insert_of_notMem _ _ _ _ hi, Finset.biUnion_insert]
rw [Equiv.Perm.Disjoint.support_mul, hrec hs']
apply disjoint_noncommProd_right
intro j hj
apply hs _ _ (ne_of_mem_of_not_mem hj hi).symm <;>
simp only [Finset.coe_insert, Set.mem_insert_iff, Finset.mem_coe, hj, or_true, true_or]
