index_subset

Mathlib.MeasureTheory.Covering.VitaliFamily

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

English

For every p in h.index, the first component p.1 lies in s.

Русский

Для каждого элемента p в h.index первая компонента p.1 принадлежит s.

LaTeX

$$$\\forall p\\in h.index\\,:\\; p.1\\in s.$$$

Lean4

theorem index_subset : ∀ p : X × Set X, p ∈ h.index → p.1 ∈ s :=
  h.exists_disjoint_covering_ae.choose_spec.1

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

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

Разделы

Аффилиация

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