prod_le_borel_prod — Mathlib

English

An instance establishing that the product space ∀i X_i is a Borel space when conditions hold.

Русский

Инстанс устанавливает, что пространство произведения ∀i X_i является борелевским пространством при соблюдении условий.

LaTeX

$$$\\text{instance borelSpace}$$$

Lean4

theorem prod_le_borel_prod : Prod.instMeasurableSpace ≤ borel (α × β) :=
  by
  rw [‹BorelSpace α›.measurable_eq, ‹BorelSpace β›.measurable_eq]
  refine sup_le ?_ ?_
  · exact comap_le_iff_le_map.mpr continuous_fst.borel_measurable
  · exact comap_le_iff_le_map.mpr continuous_snd.borel_measurable

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