isCobounded_biInter_finset — Mathlib

English

For a finite index Finset s, IsCobounded of the intersection over i ∈ s of f i holds iff each f i is cobounded for i ∈ s.

Русский

Для конечного Finset s: IsCobounded(⋂ i∈s, f i) эквивалентно ∀ i∈s, IsCobounded(f i).

LaTeX

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

Lean4

@[simp]
theorem isCobounded_biInter_finset (s : Finset ι) {f : ι → Set α} :
    IsCobounded (⋂ i ∈ s, f i) ↔ ∀ i ∈ s, IsCobounded (f i) :=
  biInter_finset_mem s

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