Commit 2023-07-01 05:00 cef7c185

View on Github →

feat: port Topology.Homotopy.Product (#3961)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Homotopy/Product.lean

added def ContinuousMap.Homotopy.prod

added def ContinuousMap.HomotopyRel.pi

added def ContinuousMap.HomotopyRel.prod

added theorem Path.Homotopic.comp_pi_eq_pi_comp

added theorem Path.Homotopic.comp_prod_eq_prod_comp

added def Path.Homotopic.pi

added def Path.Homotopic.piHomotopy

added theorem Path.Homotopic.pi_lift

added theorem Path.Homotopic.pi_proj

added def Path.Homotopic.prod

added def Path.Homotopic.prodHomotopy

added theorem Path.Homotopic.prod_lift

added theorem Path.Homotopic.prod_projLeft_projRight

added def Path.Homotopic.proj

added def Path.Homotopic.projLeft

added theorem Path.Homotopic.projLeft_prod

added def Path.Homotopic.projRight

added theorem Path.Homotopic.projRight_prod

added theorem Path.Homotopic.proj_pi