isClosed_coinduced — Mathlib

English

Analogous for closed sets: IsClosed in the coinduced topology iff the preimage of the set under f is closed.

Русский

Аналогично для замкнутых: IsClosed в коиндукции эквивалентно тому, что предобраз замкнутого множества по f замкнут.

LaTeX

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

Lean4

theorem isClosed_coinduced {t : TopologicalSpace α} {s : Set β} {f : α → β} :
    IsClosed[t.coinduced f] s ↔ IsClosed (f ⁻¹' s) := by
  simp only [← isOpen_compl_iff, isOpen_coinduced (f := f), preimage_compl]

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