inv_image_trans_target — Mathlib

English

The image of the target under the inverse map equals the intersection of the source of the second with the domain of the first.

Русский

Образ целевой области через обратное отображение равен пересечению области источника второго и области определения первого.

LaTeX

$$$ \\mathrm{Set.image}(\\mathrm{e'.symm.toFun'}, (\\mathrm{e.trans e'}).target) = (\\mathrm{e'.source} \\cap \\mathrm{e.target}) $$$

Lean4

theorem inv_image_trans_target : e'.symm '' (e.trans e').target = e'.source ∩ e.target :=
  image_trans_source e'.symm e.symm

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