Mathlib v3 is deprecated. Go to Mathlib v4

Def is_open

Modification history

2023-01-30 21:46

src/topology/basic.lean

refactor(topology/{order,*}): review API (#18312) …

Modified is_open View on Github →

2022-06-29 10:03

src/topology/basic.lean

refactor(topology/*): Use `disjoint` (#14950) …

Modified is_open View on Github →

2017-08-10 16:41

topology/topological_space.lean

rename open -> is_open, closed -> is_closed

Added is_open View on Github →