measurable_tProd_elim — Mathlib

English

For a list l with decidable equality, the elimination map v ↦ v.elim hi is measurable for any hi ∈ l.

Русский

Для списка с разрешимым равенством отображение elim для индексов измеримо.

LaTeX

$$$\\mathrm{Measurable}(\\mathrm{TProd.elim}\\ hi)$$$

Lean4

theorem measurable_tProd_elim [DecidableEq δ] :
    ∀ {l : List δ} {i : δ} (hi : i ∈ l), Measurable fun v : TProd X l => v.elim hi
  | i :: is, j, hj => by
    by_cases hji : j = i
    · subst hji
      simpa using measurable_fst
    · simp only [TProd.elim_of_ne _ hji]
      rw [mem_cons] at hj
      exact (measurable_tProd_elim (hj.resolve_left hji)).comp measurable_snd

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