compl

Mathlib.Topology.OpenPartialHomeomorph

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

English

IsImage is preserved under taking complements: IsImage(e, s, t) implies IsImage(e, sᶜ, tᶜ).

Русский

IsImage сохраняется под взятием дополнения: IsImage(e, s, t) ⇒ IsImage(e, sᶜ, tᶜ).

LaTeX

$$IsImage(e, s, t) \\Rightarrow IsImage(e, s^{c}, t^{c})$$

Lean4

protected theorem compl (h : e.IsImage s t) : e.IsImage sᶜ tᶜ := fun _ hx => (h hx).not

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

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

Разделы

Аффилиация

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