iff_preimage_eq — Mathlib

English

IsImage(s,t) is equivalent to the intersection of the source with the preimage of t under e equaling the intersection with s.

Русский

IsImage(s,t) эквивалентно тому, что пересечение источника с предобразом t по e равно пересечению с s.

LaTeX

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

Lean4

theorem iff_preimage_eq : e.IsImage s t ↔ e.source ∩ e ⁻¹' t = e.source ∩ s :=
  PartialEquiv.IsImage.iff_preimage_eq

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