Topology.Basic !4#1826

Stream: mathlib4

[Yury G. Kudryashov]

I started porting topology.basic in !4#1826, depends on #18288

[Yury G. Kudryashov]

Should I use IsOpen or Open?

[Jireh Loreaux]

Are we eschewing Is for some reason?

[Yury G. Kudryashov]

It seems that compact was renamed to is_compact some time ago, so probably I should use IsOpen.

[Frédéric Dupuis]

Is is used all over the place, see for instance docs4#IsSymmOp and friends.

[Yury G. Kudryashov]

I remember that there was some discussion about is but I don't remember if it was about adding is or removing is.

[Yury G. Kudryashov]

What should I do with the names for docs#Lim, docs#Lim', and docs#lim?

[Arien Malec]

I believe the consensus is rename has_foo to Foo but leave is_foo as IsFoo unless there's a compelling reason for alignment to Lean 4 core/std conventions?

This section of the naming wiki is thus far incomplete however.

[Arien Malec]

Here's the best consensus on this which amounts to the above:

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/ENnReal/near/312549431

[Kevin Buzzard]

If we're reopening the is/has debate then I'll say again that is is really really helpful in indicating that the thing you're talking about is a Prop, which is great for teaching.

[Yury G. Kudryashov]

Topology.Basic is ready for review.