A point interior to a rectangle does not lie on the rectangle's border
Provednot_mem_rectangleBorder_of_rectangle_mem_nhdsLet and consider the closed axis-parallel rectangle (as a subset of , with sides taken as unordered intervals), together with its border , the union of its four edges. Suppose is a point such that is a neighborhood of , i.e. . Then
In other words, if the rectangle contains an open set around , then must lie in the interior and cannot be on any of the four boundary edges.
This lemma is part of the PNT+ rectangle toolkit underlying contour integration on rectangles: residue-type arguments require the pole to sit strictly inside the contour, and this statement converts the topological hypothesis "the rectangle is a neighborhood of " into the combinatorial fact that avoids the boundary, so that the integrand is well-behaved on the contour itself.
import Mathlib.Analysis.Complex.Convex
import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.Analysis.Normed.Order.Lattice
import Mathlib.Order.Interval.Set.Monotone
import Definitions.Def_Rectangle_defs
open Complex Set Topology
open scoped Interval
variable {z w : ℂ} {c : ℝ}
open Rectangletheorem not_mem_rectangleBorder_of_rectangle_mem_nhds {z w p : ℂ}
(hp : Rectangle z w ∈ 𝓝 p) :
p ∉ RectangleBorder z w := by sorry