Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-09-19 07:18
499ab570
View on Github →
refactor(topology/constructions): golf, add
@[simp]
/
iff
variants (
#16539
)
Estimated changes
Modified
src/topology/constructions.lean
modified
theorem
continuous.sum_map
added
theorem
continuous_sum_elim
added
theorem
continuous_sum_map
modified
theorem
embedding_inl
modified
theorem
embedding_inr
added
theorem
is_open_map.sum_elim
added
theorem
is_open_map_inl
added
theorem
is_open_map_inr
modified
theorem
is_open_map_sum
added
theorem
is_open_map_sum_elim
modified
theorem
is_open_range_inl
modified
theorem
is_open_range_inr
added
theorem
nhds_inl
added
theorem
nhds_inr
modified
theorem
open_embedding_inl
modified
theorem
open_embedding_inr
Modified
src/topology/homeomorph.lean