English
Let g,c be permutations and s a finite set with hg: ∀ x, g x ∈ s ↔ x ∈ s. Then a certain equivalence between the subtype extension and c holds if and only if c.support ⊆ s and the restrictions agree on s.
Русский
Пусть g, c — перестановки, s — конечное множество и hg: ∀ x, g x ∈ s ↔ x ∈ s. Тогда утверждение об эквивалентности экстендирований подтвердается, когда supp(c) ⊆ s и ограничения совпадают на s.
LaTeX
$$$hg:\forall x, g x \in s \iff x \in s \Rightarrow (\text{ofSubtype } g|_s = c|_s) \iff (\operatorname{supp}(c) \subseteq s \land \text{restrictions match}).$$$
Lean4
theorem support_prod_of_pairwise_disjoint (l : List (Perm α)) (h : l.Pairwise Disjoint) :
l.prod.support = (l.map support).foldr (· ⊔ ·) ⊥ := by
induction l with
| nil => simp
| cons hd tl hl =>
rw [List.pairwise_cons] at h
have : Disjoint hd tl.prod := disjoint_prod_right _ h.left
simp [this.support_mul, hl h.right]
