frontier_left — Mathlib

English

If t is open and s and t are disjoint, then frontier(s) is disjoint from t.

Русский

Если t открыто и s и t непересекаются, то frontier(s) не пересекается с t.

LaTeX

$$$\\operatorname{Disjoint}(\\operatorname{frontier}(s), t)$$$

Lean4

theorem frontier_left (ht : IsOpen t) (hd : Disjoint s t) : Disjoint (frontier s) t :=
  subset_compl_iff_disjoint_right.1 <|
    frontier_subset_closure.trans <| closure_minimal (disjoint_left.1 hd) <| isClosed_compl_iff.2 ht

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