preimage_frontier — Mathlib

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

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