mathlib3

881d122b - feat(algebra/indicator_function): the inverse image under a constant indicator function has four possibilities (#16041)

feat(algebra/indicator_function): the inverse image under a constant indicator function has four possibilities (#16041) The possibilities are `set.univ, U, Uᶜ, ∅`, This lemma is from LTE. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>