borel_anti — Mathlib

English

Borel structure is antitone with respect to inclusion: larger sigma-algebras correspond to smaller topologies.

Русский

Структура Бореля антиантимонотна по включению: большие сигма-алгебры соответствуют меньшим топологиям.

LaTeX

$$$\operatorname{Antitone}(\mathrm{borel})$$$

Lean4

theorem borel_anti : Antitone (@borel α) := fun _ _ h => MeasurableSpace.generateFrom_le fun _ hs => .basic _ (h _ hs)

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