isCobounded_biInter — Mathlib

English

If s is finite and f i are subsets, then IsCobounded of the intersection over i ∈ s of f i is equivalent to IsCobounded of each f i.

Русский

Если s – конечное, то пересечение f i по i∈s кобондировано тогда и только тогда, когда каждый f i кобондирован.

LaTeX

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

Lean4

theorem isCobounded_biInter {s : Set ι} {f : ι → Set α} (hs : s.Finite) :
    IsCobounded (⋂ i ∈ s, f i) ↔ ∀ i ∈ s, IsCobounded (f i) :=
  biInter_mem hs

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