of_image_eq

Mathlib.Topology.OpenPartialHomeomorph

URI: https://scilib.ai/kg/mathlib#OpenPartialHomeomorph.IsImage.of_image_eq

English

If the image equality e''(e.source ∩ s) = e.target ∩ t holds, then e.IsImage s t holds.

Русский

Если выполнено равенство образа e''(e.source ∩ s) = e.target ∩ t, то e.IsImage s t верно.

LaTeX

$$ (e '' (e.source ∩ s) = e.target ∩ t) \\Rightarrow IsImage(e, s, t)$$

Lean4

theorem of_image_eq (h : e '' (e.source ∩ s) = e.target ∩ t) : e.IsImage s t :=
  PartialEquiv.IsImage.of_image_eq h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru