Zulip Chat Archive

Stream: maths

Topic: local properties on charted spaces


view this post on Zulip Heather Macbeth (Aug 25 2020 at 13:52):

@Scott Morrison I did this as an experiment

view this post on Zulip Heather Macbeth (Aug 25 2020 at 13:52):

https://github.com/leanprover-community/mathlib/tree/local_invariant_prop

view this post on Zulip Heather Macbeth (Aug 25 2020 at 13:53):

I was trying to get local_invariant_prop working as a local_predicate, as we discussed the other day.

view this post on Zulip Scott Morrison (Aug 25 2020 at 13:55):

le_of_hom should solve at least some of your sorries

view this post on Zulip Heather Macbeth (Aug 25 2020 at 13:55):

Oh good!

view this post on Zulip Heather Macbeth (Aug 25 2020 at 13:55):

The other two sorries are goals of the following form: f (⇑i ⟨y, hy⟩) = f ⟨y, _⟩

view this post on Zulip Heather Macbeth (Aug 25 2020 at 13:57):

Can that be deduced from i: U ⟶ V?

view this post on Zulip Scott Morrison (Aug 25 2020 at 13:57):

They both work by refl!

view this post on Zulip Scott Morrison (Aug 25 2020 at 13:57):

nicely done!

view this post on Zulip Scott Morrison (Aug 25 2020 at 13:58):

Just earlier this evening I was feeling guilty about not having attempted this :-)

view this post on Zulip Heather Macbeth (Aug 25 2020 at 14:03):

OK, I pushed an updated version with the sorries solved. If it fits well into your PR, feel free to (clean up and) use it.


Last updated: May 11 2021 at 00:31 UTC