English
Let ι be a type, k: ι → Perm α, s ⊆ ι finite, hs pairwise commuting, and hg ∀ i∈s, g.Disjoint (k i). Then g is disjoint from s.noncommProd k hs.
Русский
Пусть ι — тип, k: ι → Perm α, s ⊆ ι конечная, hs попарно коммутируют, и hg ∀ i∈s, g.Disjoint (k i). Тогда g раздельна от s.noncommProd k hs.
LaTeX
$$$(hs : s.\text{toSet}.Pairwise (\lambda i j, \operatorname{Commute}(k i)(k j))) \rightarrow (\forall i \in s,\operatorname{Disjoint}(g, k i)) \rightarrow \operatorname{Disjoint}(g, s.\mathrm{noncommProd} k hs)$$$
Lean4
theorem disjoint_noncommProd_right {ι : Type*} {k : ι → Perm α} {s : Finset ι}
(hs : Set.Pairwise s fun i j ↦ Commute (k i) (k j)) (hg : ∀ i ∈ s, g.Disjoint (k i)) :
Disjoint g (s.noncommProd k (hs)) :=
noncommProd_induction s k hs g.Disjoint (fun _ _ ↦ Disjoint.mul_right) (disjoint_one_right g) hg
