image_eq — Mathlib

English

If h holds, then the image of the restricted source equals the restricted target under e.

Русский

Если выполняется h, то образ ограниченного источника совпадает с ограниченным целевым под e.

LaTeX

$$e.IsImage s t → Set.image e.toFun (Set.instInter.inter e.source s) = Set.instInter.inter e.target t$$

Lean4

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

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