interedges_eq_biUnion — Mathlib

English

The edge relation equals a biUnion over x in s of the mapped subset of t with r x y.

Русский

Связь ребер равна би-объединению по x∈s соответствующей подмножества t, где r x y.

LaTeX

$$$ \mathrm{interedges}(r,s,t) = s \mathrm{biUnion} \bigl( x \mapsto \{ y \in t \mid r(x,y) \} \bigr) $$$

Lean4

theorem interedges_eq_biUnion :
    interedges r s t = s.biUnion fun x ↦ {y ∈ t | r x y}.map ⟨(x, ·), Prod.mk_right_injective x⟩ := by ext ⟨x, y⟩;
  simp [mem_interedges_iff]

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