compl_congr — Mathlib

English

Let π1 and π2 be prepartitions of a fixed box I. If their iUnion are equal, then their complements are equal as well.

Русский

Пусть π1 и π2 — предразбиения некоторого фиксированного прямоугольника I. Если их объединение по индексу i совпадает, то их дополнения совпадают.

LaTeX

$$$ \\forall \\pi_1,\\pi_2:\\mathrm{Prepartition}(I),\\ \\pi_1.iUnion = \\pi_2.iUnion \\Rightarrow \\pi_1.\\mathrm{compl} = \\pi_2.\\mathrm{compl}$$$

Lean4

/-- Since the definition of `BoxIntegral.Prepartition.compl` uses `Exists.choose`,
the result depends only on `π.iUnion`. -/
theorem compl_congr {π₁ π₂ : Prepartition I} (h : π₁.iUnion = π₂.iUnion) : π₁.compl = π₂.compl :=
  by
  dsimp only [compl]
  congr 1
  rw [h]

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