English
From a CU P object, construct a new CU P by selecting an open set U containing the current C and with closure contained in the original U, yielding a refined pair with the same C and adjusted U.
Русский
Из объекта CU P строится новый CU P, выбрав открытое множество U, содержащее текущее C и так, чтобы closure U было внутри исходного U, возвращая уточнённую пару с тем же C и скорректированным U.
LaTeX
$$$left(c)\\;:\\; CU P \to CU P$ with $left(c).C = c.C$, and $c.C \\subseteq left(c).U \\subseteq c.U$, and $\\overline{left(c).U} \\subseteq c.U$.$$
Lean4
/-- By assumption, for each `c : CU P` there exists an open set `u`
such that `c.C ⊆ u` and `closure u ⊆ c.U`. `c.left` is the pair `(c.C, u)`. -/
@[simps C]
def left (c : CU P) : CU P where
C := c.C
U := (c.hP c.closed_C c.P_C_U c.open_U c.subset).choose
closed_C := c.closed_C
P_C_U := (c.hP c.closed_C c.P_C_U c.open_U c.subset).choose_spec.2.2.2.1
open_U := (c.hP c.closed_C c.P_C_U c.open_U c.subset).choose_spec.1
subset := (c.hP c.closed_C c.P_C_U c.open_U c.subset).choose_spec.2.1
hP := c.hP
