disjUnion — Mathlib

English

If both π1 and π2 are Henstock decompositions, then their disjoint union is Henstock as well.

Русский

Если оба разбиения Хенштокпа, то их дизъюнкция тоже Хенштокг.

LaTeX

$$$ IsHenstock(π_1.disjUnion π_2 h) \leftarrow π_1 \text{IsHenstock}, π_2 \text{IsHenstock} $$$

Lean4

theorem disjUnion (h₁ : IsHenstock π₁) (h₂ : IsHenstock π₂) (h : Disjoint π₁.iUnion π₂.iUnion) :
    IsHenstock (π₁.disjUnion π₂ h) := by
  classical
  refine fun J hJ => (Finset.mem_union.1 hJ).elim (fun hJ => ?_) fun hJ => ?_
  · rw [disjUnion_tag_of_mem_left _ hJ]
    exact h₁ _ hJ
  · rw [disjUnion_tag_of_mem_right _ hJ]
    exact h₂ _ hJ

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