absorbs_biUnion_finset — Mathlib

English

Let I be a Finset. Absorbs M s (⋃ i∈I t_i) holds iff ∀ i∈I, Absorbs M s (t_i).

Русский

Поглощение s относительно объединения по i∈I t_i эквивалентно поглощению каждого t_i, когда I — конечное множество.

LaTeX

$$$Absorbs M s (\bigcup_{i\in I} t_i) \iff \forall i \in I, Absorbs M s (t_i)$$$

Lean4

@[simp]
theorem _root_.absorbs_biUnion_finset {ι : Type*} {t : ι → Set α} {I : Finset ι} :
    Absorbs M s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, Absorbs M s (t i) :=
  I.finite_toSet.absorbs_biUnion

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