of_isClosed — Mathlib

English

If a condition h says that for every t, whenever all s∈S have preimages closed, then t is closed, then S is coherent.

Русский

Если условие h говорит: для каждого t, если все s∈S удовлетворяют, что их прообраз закрыт, тогда t закрыто, то S когерентно.

LaTeX

$$$ (\\forall t, (\\forall s \\in S, \\text{IsClosed}((\\uparrow)^{-1}' t : \\text{Set } s)) \\to \\text{IsClosed } t) \\to \\text{IsCoherentWith} S $$$

Lean4

theorem of_isClosed (h : ∀ t : Set X, (∀ s ∈ S, IsClosed ((↑) ⁻¹' t : Set s)) → IsClosed t) : IsCoherentWith S :=
  ⟨fun _t ht ↦ isClosed_compl_iff.1 <| h _ fun s hs ↦ (ht s hs).isClosed_compl⟩

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