inter

Mathlib.Topology.OpenPartialHomeomorph

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

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 \\cap s', t \\cap t')$$

Lean4

protected theorem inter {s' t'} (h : e.IsImage s t) (h' : e.IsImage s' t') : e.IsImage (s ∩ s') (t ∩ t') := fun _ hx =>
  (h hx).and (h' hx)

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

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

Разделы

Аффилиация

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