Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-22 10:34 96d57306

View on Github →

feat(topology/continuous_function): lemmas about pointwise sup/inf (#7249)

Estimated changes

Modified src/data/finset/lattice.lean

deleted theorem finset.inf'_apply

deleted theorem finset.sup'_apply

Modified src/topology/continuous_function/basic.lean

added theorem continuous_map.inf'_apply

added theorem continuous_map.inf'_coe

added theorem continuous_map.inf_coe

added theorem continuous_map.sup'_apply

added theorem continuous_map.sup'_coe

added theorem continuous_map.sup_coe