mem_piiUnionInter_of_measurableSet

English

If i ∈ S and s is measurable with respect to m_i, then s belongs to piiUnionInter (λ n, {s | MeasurableSet[m n] s}) S.

Русский

Если i ∈ S и множество s измеримо относительно пространства m_i, то s принадлежит piiUnionInter (λ n, {s | MeasurableSet[m n] s}) S.

LaTeX

$$$\text{hiS : } i \in S \; \rightarrow \; s \in \mathrm{piiUnionInter}(\lambda n, \{s \mid MeasurableSet[m n] s\}) S$$$

Lean4

theorem mem_piiUnionInter_of_measurableSet (m : ι → MeasurableSpace α) {S : Set ι} {i : ι} (hiS : i ∈ S) (s : Set α)
    (hs : MeasurableSet[m i] s) : s ∈ piiUnionInter (fun n => {s | MeasurableSet[m n] s}) S :=
  subset_piiUnionInter hiS hs

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