trans_source' — Mathlib

English

A refined expression for the source of the composition using a nested preimage with the target intersection.

Русский

Уточнённое выражение области определения композиции через вложенное обратное изображение пересечения целевой области.

LaTeX

$$$ (e.trans e').source = e.source \\cap e \\,^{-1}'(e'.source \\cap e'.source) $$$

Lean4

theorem trans_source' : (e.trans e').source = e.source ∩ e ⁻¹' (e.target ∩ e'.source) :=
  PartialEquiv.trans_source' e.toPartialEquiv e'.toPartialEquiv

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