set_prod_ae_eq — Mathlib

English

If two sets s,s′ in α are ae-equal and t,t′ in β are ae-equal, then the product sets s × t and s′ × t′ are ae-equal with respect to μ × ν.

Русский

Если множества s и s′ в α а также t и t′ в β равны почти наверняка, то их продуcты s × t и s′ × t′ равны почти наверняка относительно μ × ν.

LaTeX

$$$(s =^{\mathrm{a.e.}}_{μ} s') \rightarrow (t =^{\mathrm{a.e.}}_{ν} t') \rightarrow (s × t =^{\mathrm{a.e.}}_{μ \otimes ν} s' × t')$$$

Lean4

theorem set_prod_ae_eq {s s' : Set α} {t t' : Set β} (hs : s =ᵐ[μ] s') (ht : t =ᵐ[ν] t') :
    (s ×ˢ t : Set (α × β)) =ᵐ[μ.prod ν] (s' ×ˢ t' : Set (α × β)) :=
  (quasiMeasurePreserving_fst.preimage_ae_eq hs).inter (quasiMeasurePreserving_snd.preimage_ae_eq ht)

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