diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 03c90f7b0..3eac659c3 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -56,6 +56,7 @@ `nbhs_one_point_compactification_weakE`, `locally_compact_completely_regular`, and `completely_regular_regular`. + + new lemmas `near_in_itvoy`, `near_in_itvyo`, `near_in_itvyy` ### Changed diff --git a/theories/normedtype.v b/theories/normedtype.v index debaf7d26..a780b3807 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -5336,10 +5336,47 @@ Lemma bound_itvE (R : numDomainType) (a b : R) : (a \in `]-oo, a]). Proof. by rewrite !(boundr_in_itv, boundl_in_itv). Qed. -Lemma near_in_itv {R : realFieldType} (a b : R) : +Section near_in_itv. +Context {R : realFieldType} (a b : R). + +Lemma near_in_itv : {in `]a, b[, forall y, \forall z \near y, z \in `]a, b[}. Proof. exact: interval_open. Qed. +Lemma near_in_itvoy : + {in `]a, +oo[, forall y, \forall z \near y, z \in `]a, +oo[}. +Proof. +move=> x ax. +near=> z. +suff : z \in `]a, +oo[%classic by rewrite inE. +near: z. +rewrite near_nbhs. +apply: (@open_in_nearW _ _ `]a, +oo[%classic) => //. +by rewrite inE/=. +Unshelve. end_near. Qed. + +Lemma near_in_itvyo : + {in `]-oo, b[, forall y, \forall z \near y, z \in `]-oo, b[}. +Proof. +move=> x xb. +near=> z. +suff : z \in `]-oo, b[%classic by rewrite inE. +near: z. +rewrite near_nbhs. +apply: (@open_in_nearW _ _ `]-oo, b[%classic) => //. +by rewrite inE/=. +Unshelve. end_near. Qed. + +Lemma near_in_itvyy : + {in `]-oo, +oo[, forall y : R, \forall z \near y, z \in `]-oo, +oo[}. +Proof. +move=> x _. +rewrite -near_nbhs. +exact: nearW => //. +Qed. + +End near_in_itv. + Lemma cvg_patch {R : realType} (f : R -> R^o) (a b : R) (x : R) : (a < b)%R -> x \in `]a, b[ -> f @ (x : subspace `[a, b]) --> f x ->