mk_eq_fun_of_mem_aeSeqSet — Mathlib

English

If i-th components f i are aemeasurable, then for any x in the AE-sequence set, the i-th carrier equals the mk construction at x.

Русский

Пусть i-я компонентa f_i является aemeasurable; для x из AESequence множества соответствующее верное равенство между f_i и mk-f_i выполняется.

LaTeX

$$$$ (hf i).mk (f i) x = f i x $$$$

Lean4

theorem mk_eq_fun_of_mem_aeSeqSet (hf : ∀ i, AEMeasurable (f i) μ) {x : α} (hx : x ∈ aeSeqSet hf p) (i : ι) :
    (hf i).mk (f i) x = f i x :=
  haveI h_ss : aeSeqSet hf p ⊆ {x | ∀ i, f i x = (hf i).mk (f i) x} :=
    by
    rw [aeSeqSet, ← compl_compl {x | ∀ i, f i x = (hf i).mk (f i) x}, Set.compl_subset_compl]
    refine Set.Subset.trans (Set.compl_subset_compl.mpr fun x h => ?_) (subset_toMeasurable _ _)
    exact h.1
  (h_ss hx i).symm

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