iff_preimage_eq'

Mathlib.Topology.OpenPartialHomeomorph

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

English

IsImage(s,t) is equivalent to e.source ∩ e^{-1}(e.target ∩ t) = e.source ∩ s.

Русский

IsImage(s,t) эквивалентно тому, что e.source ∩ e^{-1}(e.target ∩ t) = e.source ∩ s.

LaTeX

$$IsImage(e, s, t) \\iff e.source \\cap e^{-1}(e.target \\cap t) = e.source \\cap s$$

Lean4

theorem iff_preimage_eq' : e.IsImage s t ↔ e.source ∩ e ⁻¹' (e.target ∩ t) = e.source ∩ s :=
  symm_iff.symm.trans iff_symm_preimage_eq'

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

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

Разделы

Аффилиация

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