isImage_source_target — Mathlib

English

For any open partial homeomorphism e: X ⇄ Y, the forward map is surjective from its source onto its target; i.e., the pair (e.source, e.target) is the image pair of e.

Русский

Для открытого частичного гомоморфизма e: X ⇄ Y выпуклая карта впереди порождает отображение от области определения к области значения; то есть пары (e.source, e.target) являются образами e.

LaTeX

$$$e.IsImage\\ e.source\\ e.target$$$

Lean4

theorem isImage_source_target : e.IsImage e.source e.target :=
  e.toPartialEquiv.isImage_source_target

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