Commit 2023-10-30 17:26 46d7a401

View on Github →

Misc lemmas about Specializes, Inseparable and path-connectedness (#7970) Generalizing one of the proofs introduced in #7878

Estimated changes

Modified Mathlib/Data/Set/Basic.lean

added theorem Set.ite_eq_of_subset_left

added theorem Set.ite_eq_of_subset_right

Modified Mathlib/Topology/Basic.lean

modified theorem Continuous.congr

added theorem continuous_congr

Modified Mathlib/Topology/Connected/PathConnected.lean

Modified Mathlib/Topology/Inseparable.lean

added theorem IsClosed.continuous_piecewise_of_specializes

added theorem IsOpen.continuous_piecewise_of_specializes

added theorem continuous_congr_of_inseparable