eventually_filterAt_mem_setsAt

Mathlib.MeasureTheory.Covering.VitaliFamily

URI: https://scilib.ai/kg/mathlib#VitaliFamily.eventually_filterAt_mem_setsAt

English

There exists a filter-tilted eventual containedness of sets belonging to setsAt x.

Русский

Существует предельное свойство принадлежности множеств к setsAt x.

LaTeX

$$$$ (v.eventually_filterAt_mem_setsAt x): \\forall \\text{...} $$$$

Lean4

theorem eventually_filterAt_mem_setsAt (x : X) : ∀ᶠ t in v.filterAt x, t ∈ v.setsAt x :=
  (v.tendsto_filterAt_iff.mp tendsto_id).1

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

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

Разделы

Аффилиация

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