interedges_biUnion — Mathlib

English

Interedges distribute over biUnion on both sides: interedges(s.biUnion f, t.biUnion g) equals the biUnion over pairs ab of interedges(f(a), g(b)).

Русский

Interedges распределяются по биобъединению с обеих сторон: interedges(s.biUnion f, t.biUnion g) = (s × t).biUnion ab ↦ interedges(f a, g b).

LaTeX

$$G.interedges (s.biUnion f) (t.biUnion g) = (s ×ˢ t).biUnion fun ab => G.interedges (f ab.fst) (g ab.snd)$$

Lean4

theorem interedges_biUnion (s : Finset ι) (t : Finset κ) (f : ι → Finset α) (g : κ → Finset α) :
    G.interedges (s.biUnion f) (t.biUnion g) = (s ×ˢ t).biUnion fun ab ↦ G.interedges (f ab.1) (g ab.2) :=
  Rel.interedges_biUnion _ _ _ _ _

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