absorbs_biInter — Mathlib

English

If h1 absorbs s1 by t1 and h2 absorbs s2 by t2, then s1+s2 is absorbed by t1+t2.

Русский

Если s1 поглощается t1 и s2 поглощается t2, то сумма s1+s2 поглощается сумма t1+t2.

LaTeX

$$$Absorbs M s_1 t_1 \rightarrow Absorbs M s_2 t_2 \rightarrow Absorbs M (s_1 + s_2) (t_1 + t_2)$$$

Lean4

theorem absorbs_biInter {ι : Type*} {I : Set ι} (hI : I.Finite) {s : ι → Set α} :
    Absorbs G₀ (⋂ i ∈ I, s i) t ↔ ∀ i ∈ I, Absorbs G₀ (s i) t :=
  biInter_mem (f := absorbing G₀ t) hI

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