frequently_smallSets_mem

Mathlib.Order.Filter.SmallSets

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

English

There exists frequently a small set s in l with the property that s ∈ l.

Русский

Существует часто малое множество s в l, такое что s принадлежит l.

LaTeX

$$$ (\\\\exists^\\\\infty s \\\\in l.smallSets, s \\in l) $$$

Lean4

theorem frequently_smallSets_mem (l : Filter α) : ∃ᶠ s in l.smallSets, s ∈ l :=
  frequently_smallSets.2 fun t ht => ⟨t, Subset.rfl, ht⟩

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

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

Разделы

Аффилиация

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