absorbs_iUnion — Mathlib

English

If ι is finite and t(i) are sets, then Absorbs M s (⋃ i, t(i)) holds iff Absorbs M s (t(i)) for all i.

Русский

Поглощение через произведение индексов по i (iUnion) равно истинно тогда и только тогда, когда поглощение имеет место для каждого i.

LaTeX

$$$Absorbs M s (\bigcup_i t_i) \iff \forall i, Absorbs M s (t_i)$$$

Lean4

@[simp]
theorem _root_.absorbs_iUnion {ι : Sort*} [Finite ι] {t : ι → Set α} :
    Absorbs M s (⋃ i, t i) ↔ ∀ i, Absorbs M s (t i) :=
  (finite_range t).absorbs_sUnion.trans forall_mem_range

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