English
For any subset s of Y, the preimage frontier commutes with restriction: e.source ∩ e^{-1}(frontier s) = e.source ∩ frontier(e^{-1}(s)).
Русский
Для любого подмножества s пространства Y граница предобраза через e совпадает с границей предобраза через e: e.source ∩ e^{-1}(frontier s) = e.source ∩ frontier(e^{-1}(s)).
LaTeX
$$$e.source \\cap e^{-1}(\\operatorname{frontier}(s)) = e.source \\cap \\operatorname{frontier}(e^{-1}(s))$$$
Lean4
theorem preimage_frontier (s : Set Y) : e.source ∩ e ⁻¹' frontier s = e.source ∩ frontier (e ⁻¹' s) :=
(IsImage.of_preimage_eq rfl).frontier.preimage_eq