-
Notifications
You must be signed in to change notification settings - Fork 234
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat: port Topology.ContinuousOn #1907
Conversation
urkud
commented
Jan 28, 2023
afff8b4
to
31193f4
Compare
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
31193f4
to
097f109
Compare
#align nhds_within_le_iff nhdsWithin_le_iff | ||
|
||
-- porting note: golfed, droped an unneeded assumption | ||
theorem preimage_nhdsWithin_coinduced' {π : α → β} {s : Set β} {t : Set α} {a : α} (h : a ∈ t) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm going to backport this and 1 similar change below.
(hg x hx).congr (fun y hy => piecewise_eq_of_not_mem _ _ _ hy.2) | ||
(piecewise_eq_of_not_mem _ _ _ hx.2) | ||
#align continuous_on.piecewise' ContinuousOn.piecewise' | ||
|
||
theorem ContinuousOn.if' {s : Set α} {p : α → Prop} {f g : α → β} [∀ a, Decidable (p a)] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Lean failed to find a Decidable
instance to apply the piecewise'
version here, so I swapped the lemmas.
@@ -306,15 +295,6 @@ theorem nhdsWithin_compl_singleton_sup_pure (a : α) : 𝓝[≠] a ⊔ pure a = | |||
rw [← nhdsWithin_singleton, ← nhdsWithin_union, compl_union_self, nhdsWithin_univ] | |||
#align nhds_within_compl_singleton_sup_pure nhdsWithin_compl_singleton_sup_pure | |||
|
|||
/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ | |||
theorem nhdsWithin_prod_eq {α : Type _} [TopologicalSpace α] {β : Type _} [TopologicalSpace β] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What happened to this decl?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@jcommelin It was moved to Topology.Constructions
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Apparently it moved to Topology.Constructions
.
Thanks 🎉 bors merge |
Pull request successfully merged into master. Build succeeded:
|