supports_biUnion — Mathlib

English

Let K be a function from Γ' to Finset Λ'. The bi-union over all a of K(a) is S-supported exactly when every fiber K(a) is S-supported.

Русский

Пусть K : Γ' → Finset Λ'. Би-объединение по всем a равно S-поддержано тогда и только тогда, когда каждый слой K(a) поддерживается S.

LaTeX

$$$\\mathrm{Supports}(\\mathrm{Finset.univ}.\\mathrm{biUnion} K,\\ S) \\iff \\forall a,\\ \\mathrm{Supports}(K(a),S).$$$

Lean4

theorem supports_biUnion {K : Option Γ' → Finset Λ'} {S} : Supports (Finset.univ.biUnion K) S ↔ ∀ a, Supports (K a) S :=
  by simpa [Supports] using forall_swap

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