isImage_source_target_of_disjoint

English

If two open partial homeomorphisms e and e' have disjoint sources and disjoint targets, then e maps the source of e' to the target of e', i.e., e.IsImage e'.source e'.target.

Русский

Если два открытых частичных гомоморфизма e и e' имеют непересекающиеся области определения и непересекающиеся области значений, то e отображает область определения e' в область значений e', то есть e.IsImage e'.source e'.target.

LaTeX

$$For all e,e', if Disjoint e.source e'.source and Disjoint e.target e'.target, then e.IsImage e'.source e'.target.$$

Lean4

theorem isImage_source_target_of_disjoint (e' : OpenPartialHomeomorph X Y) (hs : Disjoint e.source e'.source)
    (ht : Disjoint e.target e'.target) : e.IsImage e'.source e'.target :=
  e.toPartialEquiv.isImage_source_target_of_disjoint e'.toPartialEquiv hs ht

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