coinduced — Mathlib

English

Any topology coinduced from a delta-generated topology is delta-generated.

Русский

Любая топология, полученная кограничением от дельта-генерируемой, также дельта-генерируемая.

LaTeX

$$$$\text{DeltaGeneratedSpace on } Y\text{ for } t_X \text{ coinduced via } f.$$$$

Lean4

/-- Any topology coinduced by a delta-generated topology is delta-generated. -/
theorem coinduced [DeltaGeneratedSpace X] (f : X → Y) : @DeltaGeneratedSpace Y (tX.coinduced f) :=
  let _ := tX.coinduced f
  ⟨(continuous_to_deltaGenerated.2 continuous_coinduced_rng).coinduced_le⟩

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