inducedFamily_Iic — Mathlib

English

For each n, restricting the induced family μ to the interval Iic n yields μ_n; i.e., ind ucedFamily μ (Iic n) = μ n.

Русский

Для каждого n индуцированное семейство μ, ограниченное интервалом Iic n, равно μ_n; то есть inducedFamily μ (Iic n) = μ n.

LaTeX

$$$\\forall n:\\mathbb{N},\\ inducedFamily\\ μ\\ (Iic\\ n) = μ\\ n$$$

Lean4

/-- Given a family of measures `μ : (n : ℕ) → Measure (Π i : Iic n, X i)`, the induced family
equals `μ` over the intervals `Iic n`. -/
theorem inducedFamily_Iic (n : ℕ) : inducedFamily μ (Iic n) = μ n :=
  by
  rw [inducedFamily, ← measure_cast (sup_Iic n) μ]
  congr with x i
  rw [restrict₂, cast_pi (by rw [sup_Iic n])]

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