isOpenImmersion_eq_inf — Mathlib

English

IsOpenImmersion is the infimum of topological embedding and stalk bijectivity.

Русский

IsOpenImmersion является инфимумиумом между топологическим вложением и биективностью stalk.

LaTeX

$$$ IsOpenImmersion = (topologically IsOpenEmbedding) \land stalkwise (fun f \to Bijective f) $$$

Lean4

theorem isOpenImmersion_eq_inf :
    @IsOpenImmersion = (topologically IsOpenEmbedding) ⊓ stalkwise (fun f ↦ Function.Bijective f) :=
  by
  ext
  exact
    isOpenImmersion_iff_stalk.trans (and_congr Iff.rfl (forall_congr' fun x ↦ ConcreteCategory.isIso_iff_bijective _))

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