inter

Mathlib.Logic.Equiv.PartialEquiv

URI: https://scilib.ai/kg/mathlib#PartialEquiv.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

$$e.IsImage s t → e.IsImage s' t' → e.IsImage (s ∩ s') (t ∩ 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 =>
  and_congr (h hx) (h' hx)

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

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

Разделы

Аффилиация

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