opensMeasurableSpace — Mathlib

English

The subtype {x ∈ α | p(x)} inherits an OpensMeasurableSpace structure from α, with borel_le derived from the ambient space.

Русский

Подтип {x ∈ α | p(x)} наследует структуру OpensMeasurableSpace от α, причём borel_le получается из окружающего пространства.

LaTeX

$$$$ OpensMeasurableSpace(\{x \in α \mid p(x)\}). $$$$

Lean4

instance opensMeasurableSpace {α : Type*} [TopologicalSpace α] [MeasurableSpace α] [h : OpensMeasurableSpace α]
    (p : α → Prop) : OpensMeasurableSpace (Subtype p) :=
  ⟨by
    rw [borel_comap]
    exact comap_mono h.1⟩

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