isOpenMap_iff_restrictPreimage — Mathlib

English

IsOpenMap f iff restricting preimages to the opens U i yields IsOpenMap for each i.

Русский

IsOpenMap f эквивалентно тому, что для каждого i отображение, полученное из ограниченного прообраза, является IsOpenMap.

LaTeX

$$$IsOpenMap f \\iff \\forall i, IsOpenMap ((U i).carrier.restrictPreimage f)$$$

Lean4

theorem isOpenMap_iff_restrictPreimage : IsOpenMap f ↔ ∀ i, IsOpenMap ((U i).1.restrictPreimage f) :=
  by
  refine ⟨fun h i ↦ h.restrictPreimage _, fun H s hs ↦ ?_⟩
  rw [hU.isOpen_iff_coe_preimage]
  intro i
  convert H i _ (hs.preimage continuous_subtype_val)
  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⟩

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