interedges_disjoint_left — Mathlib

English

If t and t' are disjoint, then interedges(r,s,t) and interedges(r,s,t') are disjoint.

Русский

Если t и t' непересекаются, то interedges(r,s,t) и interedges(r,s,t') несовпадающие.

LaTeX

$$$ \text{Disjoint}(\mathrm{interedges}(r,s,t), \mathrm{interedges}(r,s,t')) $ при $ \mathrm{Disjoint}(t,t') $$$

Lean4

theorem interedges_disjoint_left {s s' : Finset α} (hs : Disjoint s s') (t : Finset β) :
    Disjoint (interedges r s t) (interedges r s' t) :=
  by
  rw [Finset.disjoint_left] at hs ⊢
  intro _ hx hy
  rw [mem_interedges_iff] at hx hy
  exact hs hx.1 hy.1

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