English
For a glue data D with injections ι i and maps f j i, the preimage of the range of ι i under ι j equals the range of f j i: ι j^{-1}(range(ι i)) = range(f j i).
Русский
Для данных склейки D с отображениями ι i и f j i, прообраз диапазона ι i по отношению к ι j равен диапазону f j i: ι j^{-1}(range(ι i)) = range(f j i).
LaTeX
$$$\iota_j^{-1}(\operatorname{range}(\iota_i)) = \operatorname{range}(f_j i).$$$
Lean4
theorem preimage_range (i j : D.J) : 𝖣.ι j ⁻¹' Set.range (𝖣.ι i) = Set.range (D.f j i) := by
rw [← Set.preimage_image_eq (Set.range (D.f j i)) (D.ι_injective j), ← Set.image_univ, ← Set.image_univ, ←
Set.image_comp, ← coe_comp, Set.image_univ, Set.image_univ, ← image_inter, Set.preimage_range_inter]
