subset_iUnion

Mathlib.Analysis.BoxIntegral.Partition.Tagged

URI: https://scilib.ai/kg/mathlib#BoxIntegral.TaggedPrepartition.subset_iUnion

English

For every box J that appears in the partition π, the box J is contained in the iUnion of π.

Русский

Для каждой коробки J, входящей в разбиение π, выполняется J ⊆ iUnion(π).

LaTeX

$$$ \\forall J \\in \\pi,\\; J \\subseteq \\pi.iUnion $$$

Lean4

theorem subset_iUnion (h : J ∈ π) : ↑J ⊆ π.iUnion :=
  subset_biUnion_of_mem h

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

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

Разделы

Аффилиация

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