eventually_mem_set

Mathlib.Order.Filter.Basic

URI: https://scilib.ai/kg/mathlib#Filter.eventually_mem_set

English

For any s ⊆ α and filter l, (∀ᶠ x in l, x ∈ s) if and only if s ∈ l.

Русский

Для подмножества s и фильтра l верно: (∀ᶠ x ∈ l, x ∈ s) эквивалентно s ∈ l.

LaTeX

$$$(\\forallᶠ x ∈ l, x \\in s) \\iff s \\in l$$$

Lean4

@[simp]
theorem eventually_mem_set {s : Set α} {l : Filter α} : (∀ᶠ x in l, x ∈ s) ↔ s ∈ l :=
  Iff.rfl

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

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

Разделы

Аффилиация

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