diff

Mathlib.Topology.OpenPartialHomeomorph

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

English

If e.IsImage s t and e.IsImage s' t', then e.IsImage (s \\ s') (t \\ t').

Русский

Если e.IsImage s t и e.IsImage s' t', то e.IsImage (s \ s') (t \ t').

LaTeX

$$IsImage(e, s, t) \\land IsImage(e, s', t') \\Rightarrow IsImage(e, s \\setminus s', t \\setminus t')$$

Lean4

protected theorem diff {s' t'} (h : e.IsImage s t) (h' : e.IsImage s' t') : e.IsImage (s \ s') (t \ t') :=
  h.inter h'.compl

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

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

Разделы

Аффилиация

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