restrictPreimage — Mathlib

English

If f is a closed map, then restricting its preimage preserves the closed-map property.

Русский

Если f — замкнутое отображение, то ограничение прообраза сохраняет свойство замкнутости.

LaTeX

$$$IsClosedMap f \\rightarrow IsClosedMap (s.restrictPreimage f)$$$

Lean4

theorem restrictPreimage (H : IsClosedMap f) (s : Set β) : IsClosedMap (s.restrictPreimage f) :=
  by
  intro t
  suffices ∀ u, IsClosed u → Subtype.val ⁻¹' u = t → ∃ v, IsClosed v ∧ Subtype.val ⁻¹' v = s.restrictPreimage f '' t by
    simpa [isClosed_induced_iff]
  exact fun u hu e => ⟨f '' u, H u hu, by simp [← e, image_restrictPreimage]⟩

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