interedges_biUnion_left — Mathlib

English

Interedges distribute over a left-biUnion: the interedges of s.biUnion f with t equal the biUnion, over a, of interedges between f(a) and t.

Русский

Interedges распределяются по слева-биобъединению: interedges(s.biUnion f, t) = biUnion_a interedges(f(a), t).

LaTeX

$$G.interedges (s.biUnion f) t = s.biUnion (fun a => G.interedges (f a) t)$$

Lean4

theorem interedges_biUnion_left (s : Finset ι) (t : Finset α) (f : ι → Finset α) :
    G.interedges (s.biUnion f) t = s.biUnion fun a ↦ G.interedges (f a) t :=
  Rel.interedges_biUnion_left _ _ _ _

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