Commit 2025-07-11 18:12 051be896

View on Github →

chore(Topology): rename pi family from π to X (#26828) As discussed in #mathlib4 > Style for naming a pi type in topology/analysis files

Estimated changes

modified theorem Pi.hasProd
modified theorem Pi.multipliable
modified theorem tprod_apply
modified theorem isOpenMap_eval
modified theorem Bornology.cobounded_pi
modified theorem isConnected_univ_pi
modified theorem isPreconnected_univ_pi
modified theorem Sigma.isConnected_iff
modified theorem Sigma.isPreconnected_iff
modified theorem Continuous.finCons
modified theorem Continuous.finInit
modified theorem Continuous.finSnoc
modified theorem Continuous.finTail
modified theorem Continuous.update
modified theorem ContinuousAt.finCons
modified theorem ContinuousAt.finInit
modified theorem ContinuousAt.finSnoc
modified theorem ContinuousAt.finTail
modified theorem ContinuousAt.update
modified theorem Filter.Tendsto.apply_nhds
modified theorem Filter.Tendsto.finInit
modified theorem Filter.Tendsto.finTail
modified theorem Filter.Tendsto.update
modified theorem Finset.continuous_restrict
modified theorem Pi.continuous_restrict₂
modified theorem continuousAt_apply
modified theorem continuousAt_pi'
modified theorem continuousAt_pi
modified theorem continuous_apply
modified theorem continuous_mulSingle
modified theorem induced_to_pi
modified theorem inducing_iInf_to_pi
modified theorem interior_pi_set
modified theorem isClosed_set_pi
modified theorem isOpen_pi_iff'
modified theorem isOpen_pi_iff
modified theorem isOpen_set_pi
modified theorem mem_nhds_of_pi_mem_nhds
modified theorem nhds_pi
modified theorem pi_generateFrom_eq
modified theorem pi_generateFrom_eq_finite
modified theorem set_pi_mem_nhds
modified theorem set_pi_mem_nhds_iff
modified theorem tendsto_pi_nhds
modified theorem ContinuousOn.finCons
modified theorem continuousOn_apply
modified theorem continuousOn_pi'
modified theorem continuousOn_pi
modified theorem continuousWithinAt_pi
modified theorem nhdsWithin_pi_eq'
modified theorem nhdsWithin_pi_eq
modified theorem nhdsWithin_pi_eq_bot
modified theorem nhdsWithin_pi_neBot
modified theorem nhdsWithin_pi_univ_eq
modified theorem EMetric.diam_pi_le_of_le
modified theorem edist_le_pi_edist
modified theorem edist_pi_def
modified theorem edist_pi_le_iff
modified theorem inseparable_pi
modified theorem specializes_pi
modified theorem Set.le_einfsep_pi_of_le
modified theorem ball_pi'
modified theorem ball_pi
modified theorem closedBall_pi'
modified theorem closedBall_pi
modified theorem dist_le_pi_dist
modified theorem dist_pi_def
modified theorem dist_pi_eq_iff
modified theorem dist_pi_le_iff'
modified theorem dist_pi_le_iff
modified theorem dist_pi_lt_iff
modified theorem nndist_le_pi_nndist
modified theorem nndist_pi_def
modified theorem nndist_pi_eq_iff
modified theorem nndist_pi_le_iff
modified theorem nndist_pi_lt_iff
modified theorem sphere_pi
modified theorem Pi.isCompact_closure_iff
modified theorem Pi.isCompact_iff