fromGlued_stalk_iso — Mathlib

English

The underlying continuous map of fromGlued is an open map.

Русский

Генерирующее отображение fromGlued на непрерывной карте является открытым.

LaTeX

$$$$ \text{FromGlued.base} \text{ is open map}. $$$$

Lean4

instance fromGlued_stalk_iso (x : 𝒰.gluedCover.glued.carrier) : IsIso (𝒰.fromGlued.stalkMap x) :=
  by
  obtain ⟨i, x, rfl⟩ := 𝒰.gluedCover.ι_jointly_surjective x
  have := stalkMap_congr_hom _ _ (𝒰.ι_fromGlued i) x
  rw [stalkMap_comp, ← IsIso.eq_comp_inv] at this
  rw [this]
  infer_instance

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