absorbs_biUnion — Mathlib

English

For a finite index set I, Absorbs M s (⋃ i∈I t_i) iff ∀ i∈I, Absorbs M s (t_i).

Русский

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

LaTeX

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

Lean4

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

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