Zulip Chat Archive

Stream: mathlib4

Topic: !4#3684 Topology.Algebra.Module.StrongTopology

Jeremy Tan (Apr 27 2023 at 16:35):

!4#3684 There are two kinds of coeFns in this file. The first type is replaceable with FunLike.coe, but I don't know what to replace the second type by

Jeremy Tan (Apr 27 2023 at 16:36):

set_option synthInstance.etaExperiment true in
theorem strongUniformity.uniformAddGroup [UniformSpace F] [UniformAddGroup F] (๐”– : Set (Set E)) :
    @UniformAddGroup (E โ†’SL[ฯƒ] F) (strongUniformity ฯƒ F ๐”–) _ := by
  letI : UniformSpace (E โ†’SL[ฯƒ] F) := strongUniformity ฯƒ F ๐”–
  rw [strongUniformity, UniformSpace.replaceTopology_eq]
  let ฯ† : (E โ†’SL[ฯƒ] F) โ†’+ E โ†’แตค[๐”–] F := โŸจ(coeFn : (E โ†’SL[ฯƒ] F) โ†’ E โ†’แตค F), rfl, fun _ _ => rflโŸฉ
  exact uniformAddGroup_comap ฯ†

Jireh Loreaux (Apr 27 2023 at 16:43):

@Anatole Dedecker or maybe @Moritz Doll can you comment on this?

Anatole Dedecker (Apr 27 2023 at 16:49):

It should be defeq to FunLike.coe. E โ†’แตค F is a type synonym for E โ†’ F with the topology of uniform convergence.

Yaรซl Dillies (Apr 27 2023 at 17:23):

I think the fix is the same as I offered this morning

Anatole Dedecker (Apr 27 2023 at 20:52):

The fix was simply to use FunLike.coe (and add pointy brackets because of nested structures)

Last updated: Dec 20 2023 at 11:08 UTC