disjoint_left — Mathlib

English

If l is obtained from l1 by a permutation, then l is disjoint with any list iff l1 is.

Русский

Если l получено из l1 перестановкой, то непересечение с любой списком сохраняется между l и l1.

LaTeX

$$$ \\forall {l_1 l_2 l: List\\, \\alpha},\\ (p: List.Perm l_1 l_2)\\Rightarrow (\\text{Disjoint } l_1 l \\iff \\text{Disjoint } l_2 l) $$$

Lean4

theorem disjoint_left {l₁ l₂ l : List α} (p : List.Perm l₁ l₂) : Disjoint l₁ l ↔ Disjoint l₂ l := by
  simp_rw [List.disjoint_left, p.mem_iff]

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