prop_of_mem_aeSeqSet — Mathlib

English

If x ∈ aeSeqSet hf p, then p x (n ↦ aeSeq hf p n x) holds.

Русский

Если x ∈ aeSeqSet hf p, тогда p x (n ↦ aeSeq hf p n x) выполняется.

LaTeX

$$$ x \in aeSeqSet\, hf\, p \implies p\, x\, (n \mapsto aeSeq\, hf\, p\, n\, x) $$$

Lean4

theorem prop_of_mem_aeSeqSet (hf : ∀ i, AEMeasurable (f i) μ) {x : α} (hx : x ∈ aeSeqSet hf p) :
    p x fun n => aeSeq hf p n x := by
  simp only [aeSeq, hx, if_true]
  rw [funext fun n => mk_eq_fun_of_mem_aeSeqSet hf hx n]
  have h_ss : aeSeqSet hf p ⊆ {x | p x fun n => f n x} :=
    by
    rw [← compl_compl {x | p x fun n => f n x}, aeSeqSet, Set.compl_subset_compl]
    refine Set.Subset.trans (Set.compl_subset_compl.mpr ?_) (subset_toMeasurable _ _)
    exact fun x hx => hx.2
  have hx' := Set.mem_of_subset_of_mem h_ss hx
  exact hx'

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