instMembershipSet

Mathlib.Topology.Algebra.FilterBasis

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

English

A RingFilterBasis BR on a ring R induces a membership relation on subsets: for any subset S ⊆ R, S ∈ BR if and only if S ∈ BR.sets.

Русский

На кольце R заданаRingFilterBasis BR; для подмножеств S⊆R определено членство: S ∈ BR тогда, когда S ∈ BR.sets.

LaTeX

$$$S \in BR \iff S \in BR.sets$.$$

Lean4

instance : Membership (Set R) (RingFilterBasis R) :=
  ⟨fun B s ↦ s ∈ B.sets⟩

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

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

Разделы

Аффилиация

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