disjoint_right — Mathlib

English

If l1 is permuted to l2, then disjoint with l on the right is preserved: Disjoint l l1 ↔ Disjoint l l2.

Русский

Если l1 преобразована перестановкой к l2, то непересечение l с l1 эквивалентно непересечению l с l2.

LaTeX

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

Lean4

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

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