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