biUnion_subset_iff_forall_subset — Mathlib

English

For finite s ⊆ α, t ⊆ Finset β, and f: α → Finset β, we have s.biUnion f ⊆ t if and only if for every x ∈ s, f(x) ⊆ t.

Русский

Пусть s ⊆ α конечное множество, t ⊆ Finset β, и f: α → Finset β. Тогда s.biUnion f ⊆ t тогда же, когда для каждого x ∈ s выполняется f(x) ⊆ t.

LaTeX

$$$s.biUnion\\,f \\subseteq t \\iff \\forall x\\in s,\\; f(x) \\subseteq t$$$

Lean4

@[simp]
theorem biUnion_subset_iff_forall_subset {α β : Type*} [DecidableEq β] {s : Finset α} {t : Finset β}
    {f : α → Finset β} : s.biUnion f ⊆ t ↔ ∀ x ∈ s, f x ⊆ t := by grind

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