instMembershipSet

Mathlib.Topology.Algebra.FilterBasis

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

English

The membership relation for the GroupFilterBasis is defined by U ∈ B if and only if U ∈ B.sets.

Русский

Отношение принадлежности элементов группы основано на принадлежности множества: U ∈ B эквивалентно U ∈ B.sets.

LaTeX

$$U \in B \iff U \in B.sets$$

Lean4

@[to_additive]
instance : Membership (Set G) (GroupFilterBasis G) :=
  ⟨fun f s ↦ s ∈ f.sets⟩

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

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

Разделы

Аффилиация

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