N_one

Mathlib.Topology.Algebra.FilterBasis

URI: https://scilib.ai/kg/mathlib#GroupFilterBasis.N_one

English

The N function evaluated at the identity equals the original filter: N(B)(1) = B.filter.

Русский

Значение функции N в единице равно изначальной фильтрационной базе: N(B)(1) = B.filter.

LaTeX

$$N( B )( 1 ) = B.filter$$

Lean4

@[to_additive (attr := simp)]
theorem N_one (B : GroupFilterBasis G) : B.N 1 = B.toFilterBasis.filter := by simp only [N, one_mul, map_id']

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

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

Разделы

Аффилиация

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