disjoint_prod_right — Mathlib

English

Let l be a list of permutations. If every element of l is disjoint from f, then f is disjoint from the product l.prod.

Русский

Пусть l — список перестановок. Если каждая перестановка из l несовместна с f, то f несовместна с произведением l.

LaTeX

$$$\forall l:\operatorname{List}(\operatorname{Perm}(\alpha)),\ (\forall g\in l,\operatorname{Disjoint}(f,g))\Rightarrow \operatorname{Disjoint}(f,\; l.\mathrm{prod})$$$

Lean4

theorem disjoint_prod_right (l : List (Perm α)) (h : ∀ g ∈ l, Disjoint f g) : Disjoint f l.prod := by
  induction l with
  | nil => exact disjoint_one_right _
  | cons g l ih =>
    rw [List.prod_cons]
    exact (h _ List.mem_cons_self).mul_right (ih fun g hg => h g (List.mem_cons_of_mem _ hg))

Похожие утверждения