iff_symm_preimage_eq — Mathlib

English

If Set.image e.symm on e.target ∩ t equals e.source ∩ s, then e.IsImage s t.

Русский

Если образ Symm(e) целевого множества и ограниченного множества совпадает с исходным, тогда e.IsImage s t.

LaTeX

$$Eq (Set.image e.symm.toFun (Set.instInter.inter e.target t)) (Set.instInter.inter e.source s) → e.IsImage s 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

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