Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-06-29 22:58
0b163fdc
View on Github →
feat: define
RestrictGenTopology
(
#13452
)
Estimated changes
Modified
Mathlib.lean
Modified
Mathlib/Topology/Constructions.lean
Modified
Mathlib/Topology/Defs/Induced.lean
added
structure
RestrictGenTopology
Created
Mathlib/Topology/RestrictGenTopology.lean
added
theorem
RestrictGenTopology.isCompact_of_seq
added
theorem
RestrictGenTopology.of_continuous_prop
added
theorem
RestrictGenTopology.of_isClosed
added
theorem
RestrictGenTopology.of_seq
Modified
Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
added
theorem
UniformOnFun.isClosed_setOf_continuous