disjoint_cobounded_iff — Mathlib

English

Given a HasBasis for a filter, disjointness with the cobounded filter is equivalent to the existence of a basis element that is bounded.

Русский

Для множителя HasBasis:Disjoint(l, cobounded) эквивалентно существованию i с p(i) и bounded(s(i)).

LaTeX

$$$\text{Disjoint}(l, cobounded) \iff \exists i, p(i) \land \text{IsBounded}(s(i))$$$

Lean4

theorem disjoint_cobounded_iff [Bornology α] {ι : Sort*} {p : ι → Prop} {s : ι → Set α} {l : Filter α}
    (h : l.HasBasis p s) : Disjoint l (cobounded α) ↔ ∃ i, p i ∧ Bornology.IsBounded (s i) :=
  h.disjoint_iff_left

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