isBounded_principal

Mathlib.Order.Filter.IsBounded

URI: https://scilib.ai/kg/mathlib#Filter.isBounded_principal

English

For a set s, IsBounded r (principal s) is equivalent to the existence of t with ∀ x ∈ s, r(x,t).

Русский

Для множества s равносильно существование t, такого что ∀ x ∈ s, r(x,t).

LaTeX

$$$$ \text{IsBounded } r (\text{principal } s) \iff \exists t, \forall x \in s, r(x,t) $$$$

Lean4

theorem isBounded_principal (s : Set α) : IsBounded r (𝓟 s) ↔ ∃ t, ∀ x ∈ s, r x t := by simp [IsBounded]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru