covering_mem

Mathlib.MeasureTheory.Covering.VitaliFamily

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

English

The covering function on h simply returns the second component of the pair, i.e., for p, h.covering p = p.2.

Русский

Функция покрытия у h просто возвращает вторую компоненту пары: для p, h.covering p = p.2.

LaTeX

$$$h.covering(p)=p.2.$$$

Lean4

theorem covering_mem {p : X × Set X} (hp : p ∈ h.index) : h.covering p ∈ f p.1 :=
  (h.exists_disjoint_covering_ae.choose_spec.2.2.1 p hp).2

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

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

Разделы

Аффилиация

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