mem_addGroupFilterBasis

Mathlib.Topology.Algebra.Nonarchimedean.Bases

URI: https://scilib.ai/kg/mathlib#RingSubgroupsBasis.mem_addGroupFilterBasis

English

For each i, the set B_i is a member of the toAddGroupFilterBasis.

Русский

Для каждого i множество B_i принадлежит toAddGroupFilterBasis.

LaTeX

$$(B i : Set A) ∈ hB.toRingFilterBasis.toAddGroupFilterBasis$$

Lean4

theorem mem_addGroupFilterBasis (i) : (B i : Set A) ∈ hB.toRingFilterBasis.toAddGroupFilterBasis :=
  ⟨i, rfl⟩

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

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

Разделы

Аффилиация

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