frontier_inter_open_inter — Mathlib

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]

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