isClosed_induced_iff — Mathlib

English

Similarly for closed sets: IsClosed in the induced topology is equivalent to preimage of a closed set.

Русский

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

LaTeX

$$$IsClosed[t.induced f]\, s \\iff \\exists t, IsClosed t \\wedge f^{-1}(t) = s$$$

Lean4

theorem isClosed_induced_iff [t : TopologicalSpace β] {s : Set α} {f : α → β} :
    IsClosed[t.induced f] s ↔ ∃ t, IsClosed t ∧ f ⁻¹' t = s :=
  by
  letI := t.induced f
  simp only [← isOpen_compl_iff, isOpen_induced_iff]
  exact compl_surjective.exists.trans (by simp only [preimage_compl, compl_inj_iff])

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