isCobounded_iInter — Mathlib

English

If the index set is finite, the infinite-like intersection reduces to a finite intersection statement: IsCobounded of the iInter of f i equals that all f i are cobounded.

Русский

Если индексный набор конечен, то IsCobounded(⋂ i, f i) эквивалентно тому, что каждый f i кобондирован.

LaTeX

$$$\text{IsCobounded}(\bigcap_{i} f(i)) \iff \forall i, \text{IsCobounded}(f(i))$$$

Lean4

@[simp]
theorem isCobounded_iInter [Finite ι] {f : ι → Set α} : IsCobounded (⋂ i, f i) ↔ ∀ i, IsCobounded (f i) :=
  iInter_mem

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