mem_coe

Mathlib.Order.Filter.Ultrafilter.Defs

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

English

The membership relation is preserved by the Ultrafilter-to-Filter coercion: s ∈ (f : Filter α) iff s ∈ f.

Русский

Отображение ультрафильтр→фильтр сохраняет членство: s ∈ (f : Filter α) тогда и только тогда, когда s ∈ f.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem mem_coe : s ∈ (f : Filter α) ↔ s ∈ f :=
  Iff.rfl

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

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

Разделы

Аффилиация

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