instMembershipSet

Mathlib.Order.Filter.Ultrafilter.Defs

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

English

Membership of a set in an ultrafilter is defined via the underlying filter: s ∈ f iff s ∈ (f : Filter α).

Русский

Членство множества в ульрафильтре определяется через базовый фильтр: s ∈ f эквивалентно s ∈ (f : Filter α).

LaTeX

$$$s \in f \iff s \in (f : \mathrm{Filter}(\alpha))$$$

Lean4

instance : Membership (Set α) (Ultrafilter α) :=
  ⟨fun f s => s ∈ (f : Filter α)⟩

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

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

Разделы

Аффилиация

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