Commit 2025-04-22 13:56 863a5521

View on Github →

chore(ClusterPt): review API&names about AccPt (#24226)

  • use accPt instead of acc in lemma names;
  • use implicit arguments in Iff and dot notation lemmas;
  • add a few convenience lemmas.

Estimated changes

modified theorem AccPt.clusterPt
added theorem accPt_iff_clusterPt
modified theorem accPt_iff_frequently
modified theorem accPt_iff_nhds
modified theorem accPt_sup
deleted theorem acc_iff_cluster
deleted theorem acc_principal_iff_cluster
added theorem clusterPt_sup