fun_prop_of_mem_aeSeqSet — Mathlib

English

If x ∈ aeSeqSet hf p, then p x (n ↦ f n x) holds, i.e., p is satisfied by the original sequence f at x on aeSeqSet.

Русский

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

LaTeX

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

Lean4

theorem fun_prop_of_mem_aeSeqSet (hf : ∀ i, AEMeasurable (f i) μ) {x : α} (hx : x ∈ aeSeqSet hf p) :
    p x fun n => f n x :=
  by
  have h_eq : (fun n => f n x) = fun n => aeSeq hf p n x := funext fun n => (aeSeq_eq_fun_of_mem_aeSeqSet hf hx n).symm
  rw [h_eq]
  exact prop_of_mem_aeSeqSet hf hx

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