interedges_disjoint_right — Mathlib

English

If t1 and t2 are disjoint, then interedges with s are disjoint: G.interedges s t1 and G.interedges s t2 have no common elements.

Русский

Если t1 и t2 не пересекаются, то множество межрёбер с s раздельно: G.interedges s t1 и G.interedges s t2 не имеют общих элементов.

LaTeX

$$Disjoint t1 t2 → Disjoint (G.interedges s t1) (G.interedges s t2)$$

Lean4

theorem interedges_disjoint_right (s : Finset α) (ht : Disjoint t₁ t₂) :
    Disjoint (G.interedges s t₁) (G.interedges s t₂) :=
  Rel.interedges_disjoint_right _ _ ht

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