pure_one

Mathlib.Order.Filter.Pointwise

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

English

The principal filter at 1 equals the unit filter; i.e., the principal at 1 is the same as 1.

Русский

Пусть 1 образует порождающий фильтр, который совпадает с единичным фильтром; то есть чистый 1 равен единице.

LaTeX

$$$\\mathrm{pure}(1) = (1 : Filter \\alpha)$$$

Lean4

@[to_additive (attr := simp)]
theorem pure_one : pure 1 = (1 : Filter α) :=
  rfl

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

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

Разделы

Аффилиация

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