English
Let α be a type with a distinguished element 1. The unit element of the filter structure on α is defined as the pure filter at 1, i.e., 1 corresponds to the filter of sets containing 1.
Русский
Пусть α - тип с фиксированным элементом 1. Единичный элемент структуры фильтров над α есть чистый фильтр на точке 1, то есть 1 задан как фильтр, содержащий множество 1.
LaTeX
$$$(1 : Filter \\alpha) = \\mathrm{pure}(1)$$$
Lean4
/-- `1 : Filter α` is defined as the filter of sets containing `1 : α` in scope `Pointwise`. -/
@[to_additive /-- `0 : Filter α` is defined as the filter of sets containing `0 : α` in scope `Pointwise`. -/
]
protected def instOne : One (Filter α) :=
⟨pure 1⟩
