isBounded_iff — Mathlib

English

A filter f is r-bounded if and only if there exists a set s in f and a bound b with s ⊆ {x | r(x,b)}.

Русский

Фильтр f ограничен относительно отношения r тогда и только тогда, когда существует множество s, принадлежащее f, и некоторое b such that s ⊆ {x | r(x,b)}.

LaTeX

$$$$ f.IsBounded r \iff \exists s \in f.sets, \exists b, s \subseteq \{x \mid r(x,b)\} $$$$

Lean4

/-- `f` is eventually bounded if and only if, there exists an admissible set on which it is
bounded. -/
theorem isBounded_iff : f.IsBounded r ↔ ∃ s ∈ f.sets, ∃ b, s ⊆ {x | r x b} :=
  Iff.intro (fun ⟨b, hb⟩ => ⟨{a | r a b}, hb, b, Subset.refl _⟩) fun ⟨_, hs, b, hb⟩ => ⟨b, mem_of_superset hs hb⟩

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