Commit 2023-01-31 07:32 ebfc9088

View on Github →

Feat: add notation IsOpen[t] and IsClosed[t] (#1957) Forward-ported from leanprover-community/mathlib#18312 Also use {} arguments in continuous_def because otherwise Lean 4 can't use it in simp with non-standard instances.

Estimated changes

Modified Mathlib/Topology/Basic.lean

modified def IsOpen

deleted structure TopologicalSpace

modified theorem continuous_def

modified theorem isOpen_fold

added theorem isOpen_mk

modified theorem isOpen_univ

modified theorem topologicalSpace_eq