isCobounded_principal — Mathlib

English

For a principal filter on a set s, IsCobounded r is equivalent to existence of a bound b such that every a is forced by s to satisfy ∀ x ∈ s, r x a → r b a.

Русский

Для принципиального фильтра по множеству s изобилование равносильно существованию границы b, такой что для каждого a выполняется: если ∀ x∈s, r x a, то r b a.

LaTeX

$$$(\mathcal{P} s).IsCobounded r \Leftrightarrow \exists b, \forall a, (\forall x \in s, r x a) \to r b a.$$$

Lean4

theorem isCobounded_principal (s : Set α) : (𝓟 s).IsCobounded r ↔ ∃ b, ∀ a, (∀ x ∈ s, r x a) → r b a := by
  simp [IsCobounded]

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