prodMap — Mathlib

English

If x is in the atom of y, then the atoms are equal.

Русский

Если x принадлежит атому y, то атомы равны.

LaTeX

$$$$ x \in \operatorname{measurableAtom}(y) \Rightarrow \operatorname{measurableAtom}(x) = \operatorname{measurableAtom}(y) $$$$

Lean4

@[fun_prop]
theorem prodMap [MeasurableSpace δ] {f : α → β} {g : γ → δ} (hf : Measurable f) (hg : Measurable g) :
    Measurable (Prod.map f g) :=
  (hf.comp measurable_fst).prodMk (hg.comp measurable_snd)

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