absorbs_iInter — Mathlib

English

For a finite index set ι, Absorbs G0 (⋂ i s_i) t is equivalent to ∀ i, Absorbs G0 (s_i) t.

Русский

Для конечного множества индексов i, Absorbs G0 (⋂ i s_i) t эквивалентно ∀ i, Absorbs G0 (s_i) t.

LaTeX

$$$Absorbs G_0 (\bigcap i, s_i) t \iff ∀ i, Absorbs G_0 (s_i) t$$$

Lean4

@[simp]
theorem absorbs_iInter {ι : Sort*} [Finite ι] {s : ι → Set α} : Absorbs G₀ (⋂ i, s i) t ↔ ∀ i, Absorbs G₀ (s i) t :=
  iInter_mem (f := absorbing G₀ t)

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