ofContinuousOpen — Mathlib

English

A PartialEquiv with continuous open forward map and open source is an OpenPartialHomeomorph.

Русский

Частичное эквивелентное отображение с непрерывной открытой forward-картой и открытым источником образует OpenPartialHomeomorph.

LaTeX

$$$e: PartialEquiv\\ X\\ Y,\\; hc: ContinuousOn e e.source,\\; ho: IsOpenMap e,\\; hs: IsOpen e.source \\Rightarrow OpenPartialHomeomorph\\ X\\ Y$$$

Lean4

/-- A `PartialEquiv` with continuous open forward map and open source is a
`OpenPartialHomeomorph`. -/
def ofContinuousOpen (e : PartialEquiv X Y) (hc : ContinuousOn e e.source) (ho : IsOpenMap e) (hs : IsOpen e.source) :
    OpenPartialHomeomorph X Y :=
  ofContinuousOpenRestrict e hc (ho.restrict hs) hs

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