iff_symm_preimage_eq — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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