lim_eq_str

Mathlib.Topology.Category.Compactum

URI: https://scilib.ai/kg/mathlib#Compactum.lim_eq_str

← MathLib Explorer

English

For any ultrafilter F on X, the limit map equals the structure map: F.lim = X.str F.

Русский

Для ультрафильтра F на X предел равен структуре: F.lim = X.str F.

LaTeX

$$$F.lim = X.str F$$$

Lean4

/-- The structure map of a compactum actually computes limits. -/
theorem lim_eq_str {X : Compactum} (F : Ultrafilter X) : F.lim = X.str F :=
  by
  rw [Ultrafilter.lim_eq_iff_le_nhds, le_nhds_iff]
  tauto

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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