covering_mem_family

Mathlib.MeasureTheory.Covering.VitaliFamily

URI: https://scilib.ai/kg/mathlib#VitaliFamily.FineSubfamilyOn.covering_mem_family

← MathLib Explorer

English

For any p ∈ h.index, the covering p.2 belongs to f(p.1).

Русский

Для любого p ∈ h.index, p.2 ∈ f(p.1).

LaTeX

$$$\\forall p\\in h.index:\\ h.covering(p)\\in f(p.1).$$$

Lean4

theorem covering_mem_family {p : X × Set X} (hp : p ∈ h.index) : h.covering p ∈ v.setsAt p.1 :=
  (h.exists_disjoint_covering_ae.choose_spec.2.2.1 p hp).1

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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