deltaGeneratedSpace — Mathlib

English

Quotients of delta-generated spaces are delta-generated: if X is delta-generated and f is a quotient map, then the quotient space Y is delta-generated.

Русский

Квоты дельта-генерируемых пространств тоже дельта-генерируемые: если X дельта-генерируемое и f — факторное отображение, то частное пространство Y — дельта-генерируемое.

LaTeX

$$$$\text{DeltaGeneratedSpace}(Y) \quad\text{where } Y = X/\sim \text{ via quotient map } f.$$$$

Lean4

/-- Quotients of delta-generated spaces are delta-generated. -/
theorem deltaGeneratedSpace [DeltaGeneratedSpace X] {f : X → Y} (h : IsQuotientMap f) : DeltaGeneratedSpace Y :=
  h.2 ▸ DeltaGeneratedSpace.coinduced f

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