Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-20 01:47 c31b1f3d

View on Github →

chore(topology/algebra): cleanup (#15301)

  • Drop instances about sub*.topological_closure. Normal sub* instances apply.
  • Add units.inducing_embed_product and units.embedding_embed_product.
  • Add inducing.has_continuous_mul, inducing.has_continuous_inv, and inducing.topological_group.
  • Use new lemmas to golf some instances.
  • Don't use section .. variables for assumptions that are used only once.
  • Reuse topological_group_inf, topological_group_Inf in group_topology.has_inf, group_topology.has_Inf.

Estimated changes

modified theorem has_continuous_inv_Inf
modified theorem has_continuous_inv_inf
modified theorem has_continuous_inv_infi
modified theorem topological_group_Inf
deleted theorem topological_group_induced
modified theorem topological_group_inf
modified theorem topological_group_infi
modified theorem has_continuous_mul_Inf
modified theorem has_continuous_mul_induced
modified theorem has_continuous_mul_inf
modified theorem has_continuous_mul_infi