symm_image_eq

Mathlib.Logic.Equiv.PartialEquiv

URI: https://scilib.ai/kg/mathlib#PartialEquiv.IsImage.symm_image_eq

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

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

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

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

Разделы

Аффилиация

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