Mathlib v3 is deprecated. Go to Mathlib v4

Theorem topological_space.opens.gi_choice_val

Modification history

2022-03-10 07:37
src/topology/opens.lean
refactor(topology/opens): Turn `opens.gi` into a Galois coinsertion (#12547) …
Deleted topological_space.opens.gi_choice_valView on Github →
2019-03-03 19:05
src/topology/basic.lean
chore(topology): Splits topology.basic and topology.continuity (#785) …
Modified topological_space.opens.gi_choice_valView on Github →
2018-12-15 12:31
analysis/topology/topological_space.lean
fix(analysis/topology/topological_space): Improve the lattice structure on opens (#511)
Added topological_space.opens.gi_choice_valView on Github →