isOpen_coinduced — Mathlib

English

Open sets in the coinduced topology are exactly preimages under f of open sets in the codomain.

Русский

Открытые множества в коиндукцированной топологии равны предобразам открытых множеств кодомы по f.

LaTeX

$$$IsOpen[t.coinduced f]\, s \\iff IsOpen(f^{-1}(s))$$$

Lean4

theorem isOpen_coinduced {t : TopologicalSpace α} {s : Set β} {f : α → β} :
    IsOpen[t.coinduced f] s ↔ IsOpen (f ⁻¹' s) :=
  Iff.rfl

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