pure — Mathlib

English

There is a canonical FTC-filter relation that, for any real a, connects the point a with the pure a filter and bottom; this encodes a basic compatibility of the calculus framework with pure filters.

Русский

Существует каноническое отношение FTC-фильтра, которое для любого действительного a соединяет точку a с чистым фильтром в a и нулевым фильтром; это отражает базовую совместимость исчисления с чистыми фильтрами.

LaTeX

$$$\\mathrm{FTCFilter}(a, \\mathrm{pure}(a), \\bot)$$$

Lean4

instance pure (a : ℝ) : FTCFilter a (pure a) ⊥ where
  pure_le := le_rfl
  le_nhds := bot_le

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