coinduced — Mathlib

English

If X is Frechet-Urysohn and f: X → Y, the induced topology on Y via f is Frechet-Urysohn.

Русский

Пусть X — пространство Фреше–Ури́шхо́н и f: X → Y; топологическое пространство на Y, индуцированное f, сохраняет свойство Фреше–Ури́шхо́н.

LaTeX

$$$[FrechetUrysohnSpace X] \Rightarrow \text{FrechetUrysohnSpace}(Y, .coinduced f)$$$

Lean4

theorem coinduced [SequentialSpace X] {Y} (f : X → Y) : @SequentialSpace Y (.coinduced f ‹_›) :=
  letI : TopologicalSpace Y := .coinduced f ‹_›
  ⟨fun _ hs ↦ isClosed_coinduced.2 (hs.preimage continuous_coinduced_rng.seqContinuous).isClosed⟩

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