Documentation

FLT.Mathlib.Data.Set.Function

theorem Set.codRestrict_range_surjective {α : Type u_1} {ι : Type u_2} (f : ια) :