prodMk — Mathlib

English

If x lies in the atom of y, then atom(x) is contained in atom(y).

Русский

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

LaTeX

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

Lean4

@[fun_prop]
theorem prodMk {β γ} {_ : MeasurableSpace β} {_ : MeasurableSpace γ} {f : α → β} {g : α → γ} (hf : Measurable f)
    (hg : Measurable g) : Measurable fun a : α => (f a, g a) :=
  Measurable.prod hf hg

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