restrictPreimage — Mathlib

English

If f is an open map, restricting its preimage preserves the open-map property.

Русский

Если f открытое отображение, ограничение предобраза сохраняет открытость отображения.

LaTeX

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

Lean4

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

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