Commit 2024-09-06 08:34 3a640cf7

View on Github →

chore(Topology/Sets): add simp(s) lemmas (#15955)

Estimated changes

Modified Mathlib/Topology/Sets/Closeds.lean

added theorem TopologicalSpace.Closeds.mem_closure

Modified Mathlib/Topology/Sets/Opens.lean

modified theorem TopologicalSpace.Opens.gc

modified def TopologicalSpace.Opens.gi

added theorem TopologicalSpace.Opens.mem_comap

added theorem TopologicalSpace.Opens.mem_interior