inf_split — Mathlib

English

The infimum of a prepartition π with the partition split I i x equals the biUnion over J of split J i x.

Русский

Гранина минимума предразбиения π и разбиения split I i x равна биобъединению по J от split J i x.

LaTeX

$$$\\pi \\wedge \\mathrm{split}\\ I\\ i\\ x = \\pi\\ biUnion (\\lambda J, \\mathrm{split}\\ J\\ i\\ x)$$$

Lean4

theorem inf_split (π : Prepartition I) (i : ι) (x : ℝ) : π ⊓ split I i x = π.biUnion fun J => split J i x :=
  biUnion_congr_of_le rfl fun _ hJ => restrict_split hJ i x

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