le_biUnionIndex

Mathlib.Analysis.BoxIntegral.Partition.Basic

URI: https://scilib.ai/kg/mathlib#BoxIntegral.Prepartition.le_biUnionIndex

English

For any J in the BiUnion πi, J ≤ π.biUnionIndex πi J.

Русский

Для любых J ∈ π.biUnion π_i выполняется J ≤ π.biUnionIndex π_i J.

LaTeX

$$$ J \\in π.biUnion π_i \\Rightarrow J \\le π.biUnionIndex π_i J $$$

Lean4

theorem le_biUnionIndex (hJ : J ∈ π.biUnion πi) : J ≤ π.biUnionIndex πi J :=
  le_of_mem _ (π.mem_biUnionIndex hJ)

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

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

Разделы

Аффилиация

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