isClosedMap_iff_restrictPreimage — Mathlib

English

Restriction of an open embedding to a subset s remains an open embedding.

Русский

Ограничение открытого внедрения к подмножеству s сохраняет свойство открытого внедрения.

LaTeX

$$$\\forall f, IsOpenEmbedding f \\rightarrow IsOpenEmbedding (s.restrictPreimage f)$$$

Lean4

theorem isClosedMap_iff_restrictPreimage : IsClosedMap f ↔ ∀ i, IsClosedMap ((U i).1.restrictPreimage f) :=
  by
  refine ⟨fun h i => h.restrictPreimage _, fun H s hs ↦ ?_⟩
  rw [hU.isClosed_iff_coe_preimage]
  intro i
  convert H i _ ⟨⟨_, hs.1, eq_compl_comm.mpr rfl⟩⟩
  ext ⟨x, hx⟩
  suffices (∃ y, y ∈ s ∧ f y = x) ↔ ∃ y, y ∈ s ∧ f y ∈ U i ∧ f y = x by simpa [← Subtype.coe_inj]
  exact ⟨fun ⟨a, b, c⟩ => ⟨a, b, c.symm ▸ hx, c⟩, by tauto⟩

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