Documentation

Project.ForMathlib.ImageSplitting

noncomputable def Set.imageSplitting {A : Type u_1} {B : Type u_2} (f : AB) (S : Set A) :
(f '' S)S
Equations
Instances For
    @[simp]
    theorem Set.imageSplitting_apply {A : Type u_1} {B : Type u_2} (f : AB) {S : Set A} (x : (f '' S)) :
    f (Set.imageSplitting f S x) = x
    @[simp]
    theorem Set.imageSplitting_comp {A : Type u_1} {B : Type u_2} (f : AB) (S : Set A) :
    @[simp]
    theorem Set.rangeSplitting_apply_coe {A : Type u_1} {B : Type u_2} (f : AB) (inj : Function.Injective f) (x : A) :
    Set.rangeSplitting f f x, = x