of_symm_image_eq

Mathlib.Topology.OpenPartialHomeomorph

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

English

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

Русский

Если e.symm''(e.target ∩ t) = e.source ∩ s, то e.IsImage s t.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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