measurableSet_lt' — Mathlib

English

If α has a second countable topology, the set of pairs (p1,p2) in α×α with p1 < p2 is a measurable set.

Русский

При наличии второго счетного топологического пространства, множество пар (p1,p2) с p1 < p2 в α×α измеримо.

LaTeX

$$$\text{MeasurableSet}\{ p\in \alpha\times\alpha \mid p_{1} < p_{2} \}$$$

Lean4

@[measurability]
theorem measurableSet_lt' [SecondCountableTopology α] : MeasurableSet {p : α × α | p.1 < p.2} :=
  (isOpen_lt continuous_fst continuous_snd).measurableSet

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