English
If a subset U1 is contained in U, then the codiscreteWithin filter relative to U1 is finer than the codiscreteWithin filter relative to U; that is, every set codiscreteWithin U1 is also codiscreteWithin U.
Русский
Если подмножество U1 содержится в U, то фильтр codiscreteWithin относительно U1 более тонкий (строже) фильтра codiscreteWithin относительно U; то есть любое множество, кодискретное внутри U1, также кодискретно внутри U.
LaTeX
$$$ \text{If } U_1 \subseteq U, \quad \text{codiscreteWithin}(U_1) \leq \text{codiscreteWithin}(U). $$$
Lean4
/-- If a set is codiscrete within `U`, then it is codiscrete within any subset of `U`. -/
theorem mono {U₁ U : Set X} (hU : U₁ ⊆ U) : codiscreteWithin U₁ ≤ codiscreteWithin U :=
by
refine (biSup_mono hU).trans <| iSup₂_mono fun _ _ ↦ ?_
gcongr
