Commit 2026-10-17 10:55 6e2da037

View on Github →

refactor: isUpperSet_Ixi → IsUpperSet.Ixi (#44929)

Estimated changes

Modified Mathlib/Data/Nat/Cast/SetInterval.lean

Modified Mathlib/Order/DirSupClosed.lean

deleted theorem dirSupClosedOn_Iic

deleted theorem dirSupClosed_Iic

deleted theorem dirSupInaccOn_Iic

deleted theorem dirSupInacc_Iic

Modified Mathlib/Order/DirectedInverseSystem.lean

Modified Mathlib/Order/IsNormal.lean

Modified Mathlib/Order/UpperLower/Basic.lean

deleted theorem isUpperSet_Ici

deleted theorem isUpperSet_Ioi

Modified Mathlib/Order/UpperLower/Fibration.lean

Modified Mathlib/Order/UpperLower/Principal.lean

Modified Mathlib/RingTheory/MvPolynomial/Ideal.lean

Modified Mathlib/Topology/Order/IsNormal.lean

Modified Mathlib/Topology/Order/LowerUpperTopology.lean

Modified Mathlib/Topology/Order/ScottTopology.lean