sUnion — Mathlib

English

If T is finite and Absorbs M s t for each t in T, then Absorbs M s (⋃ i∈I t_i).

Русский

Если T конечное и s поглощается каждым t в T, то s поглощается объединением по i∈I.

LaTeX

$$$(hT : T.Finite) \rightarrow (\forall t \in T, Absorbs M s t) \rightarrow Absorbs M s (\bigcup T)$$$

Lean4

protected theorem sUnion (hT : T.Finite) (hs : ∀ t ∈ T, Absorbs M s t) : Absorbs M s (⋃₀ T) :=
  hT.absorbs_sUnion.2 hs

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