borel_comap — Mathlib

English

Let f: α → β and endow α with the topology induced by f. Then the Borel sigma-algebra on α is the comap of the Borel sigma-algebra on β by f.

Русский

Пусть f: α → β и на α задаётся топологией, индуцированной f. Тогда бореллева сигма-алгебра на α равна обратной связь (comap) борелевой сигма-алгебры β по f.

LaTeX

$$$$ \mathrm{borel}_{\alpha}(t.induced f) = (\mathrm{borel}_{\beta}(t)).comap f. $$$$

Lean4

theorem borel_comap {f : α → β} {t : TopologicalSpace β} : @borel α (t.induced f) = (@borel β t).comap f :=
  comap_generateFrom.symm

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