Commit 2025-06-12 05:16 789aae7f

View on Github →

feat: is{Inducing,Embedding}_prodMkLeft (#25705) Analoguous to isEmbedding_prodMk, which I've renamed to isEmbedding_prodMkRight for clarify. Add isInducing_prodMk{Left,Right} also.

Estimated changes

Modified Mathlib/Topology/Constructions/SumProd.lean

deleted theorem isEmbedding_prodMk

added theorem isEmbedding_prodMkLeft

added theorem isEmbedding_prodMkRight

added theorem isInducing_prodMkLeft

added theorem isInducing_prodMkRight

Modified Mathlib/Topology/FiberBundle/Basic.lean