filterAt_neBot

Mathlib.MeasureTheory.Covering.VitaliFamily

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

English

For each x, the filter v.filterAt(x) is nontrivial if the Vitali family is nontrivial.

Русский

Для каждой точки x фильтр v.filterAt(x) не тривиален, если семейство Витали не тривиально.

LaTeX

$$Instance: (v.filterAt x).NeBot$$

Lean4

instance filterAt_neBot (x : X) : (v.filterAt x).NeBot :=
  (v.filterAt_basis_closedBall x).neBot_iff.2 <| v.nontrivial _ _

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

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

Разделы

Аффилиация

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