Commit 2024-05-27 07:04 b0eb4bbc

View on Github →

refactor(Topology/Constructions): prod_generateFrom_generateFrom_eq (#13239)

Estimated changes

Modified Mathlib/Topology/Constructions.lean

modified theorem embedding_inclusion

modified theorem isClosed_range_sigmaMk

modified theorem isOpen_range_sigmaMk