isOpenImmersion_iff_stalk — Mathlib

English

An open immersion is equivalent to having an open embedding on bases and all stalk maps being isomorphisms.

Русский

Открытое вложение эквивалентно тому, что базовая карта открыта-вложение и все stalk-карты изоморфизмами.

LaTeX

$$$ IsOpenImmersion f \iff (IsOpenEmbedding f.base \land \forall x, IsIso (f.stalkMap x)) $$$

Lean4

theorem isOpenImmersion_iff_stalk {f : X ⟶ Y} :
    IsOpenImmersion f ↔ IsOpenEmbedding f.base ∧ ∀ x, IsIso (f.stalkMap x) :=
  IsOpenImmersion.iff_stalk_iso f

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