join_principal_eq_sSup

Mathlib.Order.Filter.Basic

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

English

The join of principal filters over a set s equals the supremum of the filters in s.

Русский

Объединение порождающих фильтров над множеством s равно верхней границе фильтров в s.

LaTeX

$$$\mathrm{join}(\mathcal{P} s) = \mathrm{sSup}~s$$$

Lean4

@[simp]
theorem join_principal_eq_sSup {s : Set (Filter α)} : join (𝓟 s) = sSup s :=
  rfl

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

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

Разделы

Аффилиация

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