coe_ae_eq_Icc — Mathlib

English

For a finite index set, the underlying coe-set of I is almost everywhere equal to Box.Icc I with respect to volume.

Русский

Для конечного множества индексов объединение множества I по коe совпадает почти наверняка с Box.Icc I по объёму.

LaTeX

$$$ (I : \\text{Set}(\\iota \\to \\mathbb{R})) =^{\\mathrm{ae}} Box.Icc(I) \\quad \\text{(w.r.t. volume)}$$$

Lean4

theorem coe_ae_eq_Icc : (I : Set (ι → ℝ)) =ᵐ[volume] Box.Icc I :=
  by
  rw [coe_eq_pi]
  exact Measure.univ_pi_Ioc_ae_eq_Icc

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