Commit 2025-12-08 05:19 a960cdba

View on Github →

refactor: make abbrevs for IsDirected α (· ≤ ·) and IsDirected α (· ≥ ·) (#32462) This standardizes how we write these typeclasses, and lets us use the to_dual tactic in the future.

Estimated changes

modified theorem Ring.DirectLimit.exists_of
modified theorem Set.iSup_mulIndicator
modified theorem QuasiconcaveOn.convex
modified theorem QuasiconvexOn.convex
modified theorem ENat.sum_iSup_of_monotone
modified theorem Finset.exists_le
modified theorem Finite.bddAbove_range
modified theorem Finite.bddBelow_range
modified theorem Finite.exists_ge
modified theorem Finite.exists_le
modified theorem Set.Finite.exists_ge
modified theorem Set.Finite.exists_le
modified theorem Antitone.measure_iInter
modified theorem Antitone.measure_iUnion
modified theorem Monotone.measure_iInter
modified theorem Monotone.measure_iUnion
modified theorem BddAbove.union
modified theorem BddBelow.union
modified theorem bddAbove_insert
modified theorem bddAbove_union
modified theorem bddBelow_insert
modified theorem bddBelow_union
modified theorem Antitone.directed_ge
modified theorem Antitone.directed_le
modified theorem Monotone.directed_ge
modified theorem Monotone.directed_le
modified theorem directed_of_isDirected_ge
modified theorem directed_of_isDirected_le
modified theorem exists_ge_ge
modified theorem exists_le_le
modified theorem exists_lt_of_directed_ge
modified theorem exists_lt_of_directed_le
modified theorem isBot_iff_isMin
modified theorem isBot_or_exists_lt
modified theorem isTop_iff_isMax
modified theorem isTop_or_exists_gt
modified theorem Filter.atBot_Iic_eq
modified theorem Filter.atBot_Iio_eq
modified theorem Filter.atTop_Ici_eq
modified theorem Filter.atTop_Ioi_eq
modified theorem Filter.map_atBot_eq_of_gc
modified theorem Filter.map_val_Ici_atTop
modified theorem Filter.map_val_Iic_atBot
modified theorem Filter.map_val_Iio_atBot
modified theorem Filter.map_val_Ioi_atTop
modified theorem Filter.tendsto_Ici_atTop
modified theorem Filter.tendsto_Iic_atBot
modified theorem Filter.tendsto_Iio_atBot
modified theorem Filter.tendsto_Ioi_atTop
modified theorem Order.Ideal.inter_nonempty