instIsOpenImmersionι — Mathlib

English

Equivalent reformulation of equality of injections along colimit with gluing data.

Русский

Эквивалентная формулировка равенства инъекций через колимит и данные склеивания.

LaTeX

$$$$ (colimit.ι F i).base \xi = (colimit.ι F j).base xj \iff \exists k fi fj, \exists x, (F.map fi).base x = \xi ∧ (F.map fj).base x = xj $$$$

Lean4

instance (i) : IsOpenImmersion (colimit.ι F i) :=
  inferInstanceAs (IsOpenImmersion ((openCover F).f i))

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