trans_target'' — Mathlib

English

The trans_target'' variant states the identical relation to trans_source'' in a dual form; the target equals the image under the inverse map of the intersection (target ∩ source).

Русский

Альтернативное представление trans_target'' выражает ту же связь через образ под обратным отображением от пересечения целевой области и источника.

LaTeX

$$$ (e.trans e').target = e'.target \\; \\text{image of } e'.toFun' \\left( e'.source \\cap e.target \\right) $$$

Lean4

theorem trans_target'' : (e.trans e').target = e' '' (e'.source ∩ e.target) :=
  trans_source'' e'.symm e.symm

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