English
If t is open, then the frontier of s ∩ t intersected with t equals the frontier of s intersected with t.
Русский
Если t открыто, то граница (s ∩ t) ∩ t равна границе s ∩ t в общем виде.
LaTeX
$$$\\forall s,t,\\; (\\text{IsOpen } t) \\Rightarrow \\operatorname{frontier}(s\\cap t)\\cap t = \\operatorname{frontier}(s)\\cap t.$$$
Lean4
theorem frontier_inter_open_inter {s t : Set X} (ht : IsOpen t) : frontier (s ∩ t) ∩ t = frontier s ∩ t := by
simp only [Set.inter_comm _ t, ← Subtype.preimage_coe_eq_preimage_coe_iff,
ht.isOpenMap_subtype_val.preimage_frontier_eq_frontier_preimage continuous_subtype_val,
Subtype.preimage_coe_self_inter]