measurableSet_le' — Mathlib

English

The set of pairs (x,y) in α × α with x ≤ y is measurable in the product σ-algebra.

Русский

Множество пар (x,y) ∈ α×α, удовлетворяющее x ≤ y, является измеримым в произведенной сигма-алгебре.

LaTeX

$$$\{(x,y) \in \alpha \times \alpha : x \le y\} \in \mathcal{M}_{\alpha} \otimes \mathcal{M}_{\alpha}$.$$

Lean4

@[measurability]
theorem measurableSet_le' : MeasurableSet {p : α × α | p.1 ≤ p.2} :=
  OrderClosedTopology.isClosed_le'.measurableSet

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