Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-23 19:01 c9ba943d

View on Github →

fix(*): fix typos I made yesterday (#15627) Fix 4 typos I made yesterday.

Estimated changes

Modified src/data/set/intervals/ord_connected.lean

added theorem set.ord_connected.interval_oc_subset

deleted theorem set.ord_interval.interval_oc_subset

Modified src/data/set/prod.lean

added theorem set.diag_preimage_prod_self

deleted theorem set.diag_preimage_prod_sellf

Modified src/topology/algebra/module/finite_dimension.lean

modified theorem linear_map.ker_to_continuous_linear_map

modified theorem linear_map.range_to_continuous_linear_map