absorbs_sUnion — Mathlib

English

Absorbs M s (⋂ i, s_i) t holds iff for every i, Absorbs M (s_i) t.

Русский

Поглощение M множества s пересечения всех s_i с t эквивалентно поглощению каждого s_i с t.

LaTeX

$$$Absorbs M s (\bigcap_i s_i) t \iff \forall i, Absorbs M s (s_i) t$$$

Lean4

theorem _root_.Set.Finite.absorbs_sUnion {T : Set (Set α)} (hT : T.Finite) :
    Absorbs M s (⋃₀ T) ↔ ∀ t ∈ T, Absorbs M s t := by simp [Absorbs, hT]

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