Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_open_lt'

Modification history

2023-01-05 13:18
src/topology/order/basic.lean
feat(topology/order/basic): replace `partial_order` by `preorder` (#18064) …
Modified is_open_lt'View on Github →
2017-09-07 20:38
topology/topological_structures.lean
feat(topology/topological_structures,ennreal): show continuity of of_ennreal and of_real
Modified is_open_lt'View on Github →
2017-09-06 19:31
topology/topological_structures.lean
feat(topology): restructure order topologies; (start) proof that ennreal is a topological monoid
Added is_open_lt'View on Github →