Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-17 01:14 87c12abd

View on Github →

feat(topology/continuous_map): lattice structures (#6706)

Estimated changes

Modified src/topology/continuous_map.lean

added def continuous_map.equiv_fn_of_discrete

added theorem continuous_map.inf_apply

added theorem continuous_map.le_def

added theorem continuous_map.lt_def

added theorem continuous_map.sup_apply