disjUnion_tag_of_mem_left

Mathlib.Analysis.BoxIntegral.Partition.Tagged

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

English

If J ∈ π1, then the tag of J in the disjoint union equals π1.tag J.

Русский

Если J ∈ π1, то тег J в дизъюнкции равен π1.tag J.

LaTeX

$$$ (π_1.disjUnion π_2 h).tag J = π_1.tag J \text{ if } J ∈ π_1 $$$

Lean4

theorem disjUnion_tag_of_mem_left (h : Disjoint π₁.iUnion π₂.iUnion) (hJ : J ∈ π₁) :
    (π₁.disjUnion π₂ h).tag J = π₁.tag J :=
  dif_pos hJ

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

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

Разделы

Аффилиация

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