isClosed_iff — Mathlib

English

If S is a coherent family, then a set t is closed in X if and only if its preimage in every s ∈ S is closed in s.

Русский

Если S — когерентное семейство, то множество t замкнуто в X тогда и только тогда, когда его прообраз в каждом s ∈ S замкнуто в s.

LaTeX

$$$ IsClosed\\,t \\iff \\forall s \\in S, IsClosed\\left((\\uparrow) \\, \\backslash' t : Set\\, s\\right) $$$

Lean4

protected theorem isClosed_iff (hS : IsCoherentWith S) : IsClosed t ↔ ∀ s ∈ S, IsClosed ((↑) ⁻¹' t : Set s) := by
  simp only [← isOpen_compl_iff, hS.isOpen_iff, preimage_compl]

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