English
From a CU P object, construct a new CU P by taking the closure of some open set around C and keeping U unchanged, forming a right-hand variant of the CU data.
Русский
Из CU P образуется новый CU P, взяв замыкание некоторого открытого множества, окружавшего C, и оставив U без изменений.
LaTeX
$$$right(c)\\;:\\; CU P \\to CU P$ with $right(c).C = \\overline{u}$ for some $u$ with $c.C \\subseteq u \\subseteq c.U$ and $right(c).U = 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.right` is the pair `(closure u, c.U)`. -/
@[simps U]
def right (c : CU P) : CU P
where
C := closure (c.hP c.closed_C c.P_C_U c.open_U c.subset).choose
U := c.U
closed_C := isClosed_closure
P_C_U := (c.hP c.closed_C c.P_C_U c.open_U c.subset).choose_spec.2.2.2.2
open_U := c.open_U
subset := (c.hP c.closed_C c.P_C_U c.open_U c.subset).choose_spec.2.2.1
hP := c.hP
