Coercion to/from `Germ`

Stream: maths

[Yury G. Kudryashov]

Currently, two parts of Mathlib have different approaches to coercions to/from docs#Filter.Germ

• generic Filter.Germ code defines coercions from α → β and β to Germ l β;
• docs#MeasureTheory.AEEqFun and docs#MeasureTheory.Lp defines a coercion from an a.e.-defined function (a.k.a. Germ μ.ae _) to functions and no coercion in the other direction.

Should we unify these approaches? One way to deal with it is to

• rename all theorems about coercion of α → β to Germ l β to use mk instead of coe;
• same with coercion of β to Germ l β and const;
• move these :up: two coercions to a scope.

Note that we can't generalize the AEEqFun coercion because it chooses a measurable representative.

[Yury G. Kudryashov]

Of course, another approach is to leave everything as is.