chore: make OrderDual a structure#35125
chore: make OrderDual a structure#35125kim-em wants to merge 43 commits intoleanprover-community:masterfrom
Conversation
Move `OrderDual` and its order instances from `Order.Basic` to a new file `Order.OrderDual`, in preparation for changing `OrderDual` from a type alias to a one-field structure. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
# Conflicts: # Mathlib/Order/Basic.lean
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Adapt 147 files to the change of `OrderDual` from a type alias to a one-field structure, preventing defeq abuse. Work in progress — approximately 25 files still need fixes. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
github-actions
bot
added
the
merge-conflict
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
github-actions
bot
added
large-import
PR summary ae6b7e9128Import changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Order.OrderDual | 113 | 129 | +16 (+14.16%) |
| Mathlib.Order.RelClasses | 115 | 130 | +15 (+13.04%) |
| Mathlib.Algebra.Order.Ring.Synonym | 147 | 163 | +16 (+10.88%) |
| Mathlib.Algebra.Order.GroupWithZero.Synonym | 142 | 146 | +4 (+2.82%) |
| Mathlib.Data.Nat.Cast.Synonym | 141 | 144 | +3 (+2.13%) |
| Mathlib.Algebra.Order.Module.Synonym | 310 | 314 | +4 (+1.29%) |
| Mathlib.Algebra.Field.Basic | 211 | 213 | +2 (+0.95%) |
| Mathlib.Algebra.Order.Group.Synonym | 139 | 140 | +1 (+0.72%) |
| Mathlib.Algebra.Order.Group.Action.Synonym | 148 | 149 | +1 (+0.68%) |
| Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual | 153 | 154 | +1 (+0.65%) |
| Mathlib.Algebra.Order.Group.DenselyOrdered | 189 | 190 | +1 (+0.53%) |
| Mathlib.Algebra.Order.Hom.Monoid | 211 | 212 | +1 (+0.47%) |
| Mathlib.Order.Monotone.Odd | 232 | 233 | +1 (+0.43%) |
| Mathlib.Order.CompleteLattice.Group | 242 | 243 | +1 (+0.41%) |
| Mathlib.Order.ConditionallyCompleteLattice.Group | 259 | 260 | +1 (+0.39%) |
| Mathlib.Order.Filter.AtTopBot.Monoid | 273 | 274 | +1 (+0.37%) |
| Mathlib.Algebra.Order.BigOperators.Group.List | 333 | 334 | +1 (+0.30%) |
| Mathlib.Algebra.Order.Ring.Cast | 468 | 469 | +1 (+0.21%) |
| Mathlib.Algebra.Order.Module.Field | 505 | 506 | +1 (+0.20%) |
| Mathlib.Algebra.Order.Module.Pointwise | 526 | 527 | +1 (+0.19%) |
| Mathlib.Algebra.Order.Rearrangement | 607 | 608 | +1 (+0.16%) |
| Mathlib.Algebra.Order.Archimedean.Basic | 644 | 645 | +1 (+0.16%) |
| Mathlib.Algebra.AddConstMap.Basic | 657 | 658 | +1 (+0.15%) |
| Mathlib.Data.ENNReal.Basic | 703 | 704 | +1 (+0.14%) |
| Mathlib.Data.Real.Pointwise | 704 | 705 | +1 (+0.14%) |
| Mathlib.Data.ENNReal.Inv | 707 | 708 | +1 (+0.14%) |
| Mathlib.Data.EReal.Operations | 709 | 710 | +1 (+0.14%) |
| Mathlib.Combinatorics.Pigeonhole | 755 | 756 | +1 (+0.13%) |
| Mathlib.Data.Finsupp.Lex | 766 | 767 | +1 (+0.13%) |
| Mathlib.Combinatorics.SetFamily.AhlswedeZhang | 778 | 779 | +1 (+0.13%) |
| Mathlib.Data.Finsupp.WellFounded | 806 | 807 | +1 (+0.12%) |
| Mathlib.Combinatorics.Enumerative.IncidenceAlgebra | 812 | 813 | +1 (+0.12%) |
| Mathlib.Topology.Order.Basic | 826 | 827 | +1 (+0.12%) |
| Mathlib.Topology.Order.MonotoneConvergence | 827 | 828 | +1 (+0.12%) |
| Mathlib.Topology.Order.NhdsSet | 827 | 828 | +1 (+0.12%) |
| Mathlib.Topology.Order.CountableSeparating | 828 | 829 | +1 (+0.12%) |
| Mathlib.Topology.Order.Filter | 830 | 831 | +1 (+0.12%) |
| Mathlib.Topology.Order.LeftRightNhds | 832 | 833 | +1 (+0.12%) |
| Mathlib.Topology.Order.IsLUB | 833 | 834 | +1 (+0.12%) |
| Mathlib.Topology.Order.MonotoneContinuity | 833 | 834 | +1 (+0.12%) |
| Mathlib.Topology.Order.DenselyOrdered | 834 | 835 | +1 (+0.12%) |
| Mathlib.Topology.Order.AtTopBotIxx | 836 | 837 | +1 (+0.12%) |
| Mathlib.Topology.Order.T5 | 836 | 837 | +1 (+0.12%) |
| Mathlib.Topology.Order.Monotone | 843 | 844 | +1 (+0.12%) |
| Mathlib.Topology.Order.ExtendFrom | 844 | 845 | +1 (+0.12%) |
| Mathlib.Topology.Order.LiminfLimsup | 849 | 850 | +1 (+0.12%) |
| Mathlib.Topology.Order.IntermediateValue | 852 | 853 | +1 (+0.12%) |
| Mathlib.Topology.Order.LeftRightLim | 852 | 853 | +1 (+0.12%) |
| Mathlib.Algebra.MonoidAlgebra.Degree | 863 | 864 | +1 (+0.12%) |
| Mathlib.Topology.Order.Compact | 876 | 877 | +1 (+0.11%) |
| Mathlib.Topology.EMetricSpace.Defs | 882 | 883 | +1 (+0.11%) |
| Mathlib.Topology.MetricSpace.Pseudo.Defs | 884 | 885 | +1 (+0.11%) |
| Mathlib.Topology.MetricSpace.Defs | 885 | 886 | +1 (+0.11%) |
| Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank | 895 | 896 | +1 (+0.11%) |
| Mathlib.Topology.Algebra.Monoid | 936 | 937 | +1 (+0.11%) |
| Mathlib.LinearAlgebra.AffineSpace.Ordered | 959 | 960 | +1 (+0.10%) |
| Mathlib.RingTheory.Noetherian.Defs | 978 | 979 | +1 (+0.10%) |
| Mathlib.Algebra.Order.Chebyshev | 989 | 990 | +1 (+0.10%) |
| Mathlib.Topology.MetricSpace.ProperSpace | 1001 | 1002 | +1 (+0.10%) |
| Mathlib.Analysis.Convex.Star | 1017 | 1018 | +1 (+0.10%) |
| Mathlib.Topology.MetricSpace.Bounded | 1023 | 1024 | +1 (+0.10%) |
| Mathlib.Topology.Algebra.Group.Basic | 1029 | 1030 | +1 (+0.10%) |
| Mathlib.Analysis.Convex.Basic | 1031 | 1032 | +1 (+0.10%) |
| Mathlib.Topology.Algebra.Order.UpperLower | 1033 | 1034 | +1 (+0.10%) |
| Mathlib.Analysis.Convex.Function | 1047 | 1048 | +1 (+0.10%) |
| Mathlib.Analysis.Normed.Group.Constructions | 1078 | 1079 | +1 (+0.09%) |
| Mathlib.Analysis.Convex.Combination | 1085 | 1086 | +1 (+0.09%) |
| Mathlib.RingTheory.Valuation.Basic | 1090 | 1091 | +1 (+0.09%) |
| Mathlib.GroupTheory.ArchimedeanDensely | 1096 | 1097 | +1 (+0.09%) |
| Mathlib.Analysis.Convex.Jensen | 1102 | 1103 | +1 (+0.09%) |
| Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors | 1112 | 1113 | +1 (+0.09%) |
| Mathlib.RingTheory.Valuation.Quotient | 1161 | 1162 | +1 (+0.09%) |
| Mathlib.Topology.Algebra.Ring.Real | 1162 | 1163 | +1 (+0.09%) |
| Mathlib.RingTheory.Ideal.MinimalPrime.Basic | 1166 | 1167 | +1 (+0.09%) |
| Mathlib.RingTheory.Noetherian.Basic | 1226 | 1227 | +1 (+0.08%) |
| Mathlib.Topology.MetricSpace.Algebra | 1272 | 1273 | +1 (+0.08%) |
| Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology | 1273 | 1274 | +1 (+0.08%) |
| Mathlib.Algebra.MvPolynomial.NoZeroDivisors | 1275 | 1276 | +1 (+0.08%) |
| Mathlib.Topology.Instances.ENNReal.Lemmas | 1281 | 1282 | +1 (+0.08%) |
| Mathlib.Topology.Semicontinuity.Basic | 1286 | 1287 | +1 (+0.08%) |
| Mathlib.Topology.Semicontinuity.Lindelof | 1287 | 1288 | +1 (+0.08%) |
| Mathlib.Topology.EMetricSpace.BoundedVariation | 1289 | 1290 | +1 (+0.08%) |
| Mathlib.Topology.Instances.EReal.Lemmas | 1292 | 1293 | +1 (+0.08%) |
| Mathlib.RingTheory.Spectrum.Prime.Basic | 1301 | 1302 | +1 (+0.08%) |
| Mathlib.Analysis.Convex.Quasiconvex | 1324 | 1325 | +1 (+0.08%) |
| Mathlib.RingTheory.Artinian.Module | 1326 | 1327 | +1 (+0.08%) |
| Mathlib.Algebra.Lie.Submodule | 1329 | 1330 | +1 (+0.08%) |
| Mathlib.Algebra.Module.Torsion.Basic | 1331 | 1332 | +1 (+0.08%) |
| Mathlib.Analysis.Normed.Order.Lattice | 1346 | 1347 | +1 (+0.07%) |
| Mathlib.RingTheory.Valuation.ValuationSubring | 1354 | 1355 | +1 (+0.07%) |
| Mathlib.Topology.UniformSpace.Dini | 1354 | 1355 | +1 (+0.07%) |
| Mathlib.RingTheory.Localization.Submodule | 1365 | 1366 | +1 (+0.07%) |
| Mathlib.Analysis.Convex.Topology | 1368 | 1369 | +1 (+0.07%) |
| Mathlib.Analysis.LocallyConvex.Polar | 1396 | 1397 | +1 (+0.07%) |
| Mathlib.LinearAlgebra.Dual.Lemmas | 1426 | 1427 | +1 (+0.07%) |
| Mathlib.Topology.MetricSpace.Thickening | 1441 | 1442 | +1 (+0.07%) |
| Mathlib.MeasureTheory.Function.AEMeasurableSequence | 1456 | 1457 | +1 (+0.07%) |
| Mathlib.MeasureTheory.Measure.MeasureSpace | 1463 | 1464 | +1 (+0.07%) |
| Mathlib.MeasureTheory.Order.Lattice | 1478 | 1479 | +1 (+0.07%) |
| Mathlib.MeasureTheory.Constructions.BorelSpace.Basic | 1481 | 1482 | +1 (+0.07%) |
| Mathlib.MeasureTheory.Constructions.BorelSpace.Order | 1485 | 1486 | +1 (+0.07%) |
| Mathlib.MeasureTheory.Function.EssSup | 1499 | 1500 | +1 (+0.07%) |
| Mathlib.Algebra.Lie.Nilpotent | 1515 | 1516 | +1 (+0.07%) |
| Mathlib.MeasureTheory.Constructions.Polish.Basic | 1533 | 1534 | +1 (+0.07%) |
| Mathlib.MeasureTheory.Function.AEEqOfLIntegral | 1619 | 1620 | +1 (+0.06%) |
| Mathlib.FieldTheory.Galois.Basic | 1702 | 1703 | +1 (+0.06%) |
| Mathlib.RingTheory.Nullstellensatz | 1732 | 1733 | +1 (+0.06%) |
| Mathlib.RingTheory.Spectrum.Prime.Topology | 1734 | 1735 | +1 (+0.06%) |
| Mathlib.RingTheory.Spectrum.Prime.Noetherian | 1749 | 1750 | +1 (+0.06%) |
| Mathlib.RingTheory.Ideal.KrullsHeightTheorem | 1825 | 1826 | +1 (+0.05%) |
| Mathlib.MeasureTheory.Function.LpSeminorm.Basic | 1838 | 1839 | +1 (+0.05%) |
| Mathlib.Analysis.InnerProductSpace.Orthogonal | 1860 | 1861 | +1 (+0.05%) |
| Mathlib.FieldTheory.Galois.Infinite | 1863 | 1864 | +1 (+0.05%) |
| Mathlib.MeasureTheory.Function.LpSpace.Complete | 1923 | 1924 | +1 (+0.05%) |
| Mathlib.FieldTheory.Galois.IsGaloisGroup | 2089 | 2090 | +1 (+0.05%) |
| Mathlib.Analysis.InnerProductSpace.Projection.Submodule | 2155 | 2156 | +1 (+0.05%) |
| Mathlib.MeasureTheory.Integral.IntegrableOn | 2195 | 2196 | +1 (+0.05%) |
| Mathlib.MeasureTheory.Function.LocallyIntegrable | 2196 | 2197 | +1 (+0.05%) |
| Mathlib.AlgebraicGeometry.IdealSheaf.Basic | 2206 | 2207 | +1 (+0.05%) |
| Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic | 2376 | 2377 | +1 (+0.04%) |
| Mathlib.AlgebraicGeometry.AffineSpace | 2377 | 2378 | +1 (+0.04%) |
| Mathlib.MeasureTheory.Integral.IntegralEqImproper | 2536 | 2537 | +1 (+0.04%) |
Import changes for all files
| Files | Import difference |
|---|---|
| There are 4112 files with changed transitive imports taking up over 186084 characters: this is too many to display! | |
You can run scripts/import_trans_difference.sh all locally to see the whole output. |
Declarations diff
+ Balanced.dual_iff
+ Balanced.map
+ Balanced.of_map
+ Bounded.of_dual
+ HasBasis.bliminf_eq_iSup_iInf
+ OrderDual.homeomorph
+ OrderDual.instSMul
+ OrderDual.instSMul'
+ OrderDual.isEmbedding_ofDual
+ OrderDual.isInducing_ofDual
+ Sized.map
+ Sized.of_map
+ Valid'.merge_aux₂
+ Valid'.of_dual
+ coe_val_apply
+ coheight_add_const
+ coheight_le_of_head_eq
+ colex_trichotomy_rec
+ diff_singleton_eventually_mem_nhds_right
+ dual_map
+ equiv
+ generateFrom_Ioc_mem_le_borel
+ gfpApprox_mem_fixedPoints_of_eq
+ induced_toDual_instTopologicalSpace
+ inf
+ instDecidableEq
+ instDecidableLE
+ instDecidableLT
+ instNNRatCast
+ instance (priority := 10) WithTop.instLE : LE (WithTop α)
+ instance (priority := 10) WithTop.instLT : LT (WithTop α)
+ instance (priority := 100) [LocallyFiniteOrder ι] [PredOrder ι] : IsPredArchimedean ι := by
+ instance (priority := 100) normedGroup [NormedGroup E] : NormedGroup Eᵒᵈ
+ instance (priority := 100) seminormedCommGroup [SeminormedCommGroup E] :
+ instance : Bornology αᵒᵈ := OrderDual.instBornology
+ instance : BoundedGENhdsClass αᵒᵈ
+ instance : BoundedLENhdsClass αᵒᵈ
+ instance : ContinuousConstSMul M αᵒᵈ
+ instance : ContinuousInv ℝ≥0∞ := ⟨continuous_ofDual.comp OrderIso.invENNReal.continuous⟩
+ instance : ContinuousNeg EReal := ⟨continuous_ofDual.comp negOrderIso.continuous⟩
+ instance : Dist Xᵒᵈ where dist a b := dist (ofDual a) (ofDual b)
+ instance : EDist Xᵒᵈ where edist a b := edist (ofDual a) (ofDual b)
+ instance : OrderClosedTopology αᵒᵈ := by
+ instance : PseudoMetricSpace αᵒᵈ
+ instance [BoundedSpace α] : BoundedSpace αᵒᵈ := by
+ instance [CancelMonoid α] : CancelMonoid αᵒᵈ
+ instance [CommGroup α] : CommGroup αᵒᵈ
+ instance [CommGroupWithZero α] : CommGroupWithZero αᵒᵈ
+ instance [CommMonoidWithZero α] : CommMonoidWithZero αᵒᵈ
+ instance [CommRing R] : CommRing Rᵒᵈ
+ instance [CommSemigroup α] : CommSemigroup αᵒᵈ
+ instance [CommSemiring R] : CommSemiring Rᵒᵈ
+ instance [Distrib R] : Distrib Rᵒᵈ
+ instance [Div α] : Div αᵒᵈ where div a b := toDual (ofDual a / ofDual b)
+ instance [DivInvMonoid α] : DivInvMonoid αᵒᵈ
+ instance [DivisionCommMonoid α] : DivisionCommMonoid αᵒᵈ
+ instance [DivisionMonoid α] : DivisionMonoid αᵒᵈ
+ instance [EMetricSpace X] : EMetricSpace Xᵒᵈ
+ instance [GroupWithZero α] : GroupWithZero αᵒᵈ
+ instance [Inhabited α] : Inhabited αᵒᵈ := ⟨toDual default⟩
+ instance [Inv α] : Inv αᵒᵈ where inv a := toDual (ofDual a)⁻¹
+ instance [InvolutiveInv α] : InvolutiveInv αᵒᵈ
+ instance [LeftCancelMonoid α] : LeftCancelMonoid αᵒᵈ
+ instance [LeftCancelSemigroup α] : LeftCancelSemigroup αᵒᵈ
+ instance [LinearOrder α] : LinearOrder (Lex (NonemptyInterval α))
+ instance [MetricSpace X] : MetricSpace Xᵒᵈ
+ instance [Monoid α] : Monoid αᵒᵈ
+ instance [MonoidWithZero α] : MonoidWithZero αᵒᵈ
+ instance [Mul R] [Add R] [LeftDistribClass R] : LeftDistribClass Rᵒᵈ
+ instance [Mul R] [Add R] [RightDistribClass R] : RightDistribClass Rᵒᵈ
+ instance [Mul R] [HasDistribNeg R] : HasDistribNeg Rᵒᵈ
+ instance [Mul α] : Mul αᵒᵈ where mul a b := toDual (ofDual a * ofDual b)
+ instance [Mul α] [IsCancelMul α] : IsCancelMul αᵒᵈ
+ instance [Mul α] [IsLeftCancelMul α] : IsLeftCancelMul αᵒᵈ
+ instance [Mul α] [IsRightCancelMul α] : IsRightCancelMul αᵒᵈ
+ instance [Mul α] [Zero α] [IsCancelMulZero α] : IsCancelMulZero αᵒᵈ
+ instance [Mul α] [Zero α] [IsLeftCancelMulZero α] : IsLeftCancelMulZero αᵒᵈ
+ instance [Mul α] [Zero α] [IsRightCancelMulZero α] : IsRightCancelMulZero αᵒᵈ
+ instance [Mul α] [Zero α] [NoZeroDivisors α] : NoZeroDivisors αᵒᵈ
+ instance [MulOneClass α] : MulOneClass αᵒᵈ
+ instance [MulZeroClass α] : MulZeroClass αᵒᵈ
+ instance [MulZeroOneClass α] : MulZeroOneClass αᵒᵈ
+ instance [NonAssocRing R] : NonAssocRing Rᵒᵈ
+ instance [NonAssocSemiring R] : NonAssocSemiring Rᵒᵈ
+ instance [NonUnitalCommRing R] : NonUnitalCommRing Rᵒᵈ
+ instance [NonUnitalCommSemiring R] : NonUnitalCommSemiring Rᵒᵈ
+ instance [NonUnitalNonAssocRing R] : NonUnitalNonAssocRing Rᵒᵈ
+ instance [NonUnitalNonAssocSemiring R] : NonUnitalNonAssocSemiring Rᵒᵈ
+ instance [NonUnitalRing R] : NonUnitalRing Rᵒᵈ
+ instance [NonUnitalSemiring R] : NonUnitalSemiring Rᵒᵈ
+ instance [One α] : One αᵒᵈ where one := toDual 1
+ instance [OrderTopology α] : OrderTopology αᵒᵈ
+ instance [PseudoEMetricSpace X] : PseudoEMetricSpace Xᵒᵈ
+ instance [PseudoMetricSpace X] [ProperSpace X] : ProperSpace Xᵒᵈ
+ instance [RightCancelMonoid α] : RightCancelMonoid αᵒᵈ
+ instance [RightCancelSemigroup α] : RightCancelSemigroup αᵒᵈ
+ instance [Ring R] : Ring Rᵒᵈ
+ instance [Ring R] [IsDomain R] : IsDomain Rᵒᵈ
+ instance [Semigroup α] : Semigroup αᵒᵈ
+ instance [SemigroupWithZero α] : SemigroupWithZero αᵒᵈ
+ instance [Semiring R] : Semiring Rᵒᵈ
+ instance [TopologicalSpace α] [FirstCountableTopology α] : FirstCountableTopology αᵒᵈ
+ instance [TopologicalSpace α] [SecondCountableTopology α] : SecondCountableTopology αᵒᵈ
+ instance [TopologicalSpace α] [SeparableSpace α] : SeparableSpace αᵒᵈ
+ instance [h : IntCast α] : IntCast αᵒᵈ
+ instance [h : MeasurableSpace α] : MeasurableSpace αᵒᵈ
+ instance [h : Nontrivial α] : Nontrivial αᵒᵈ
+ instance [h : Unique α] : Unique αᵒᵈ
+ isOpen_of_isOpen_ofDual_preimage
+ le_lfp_const_sup
+ le_sInf
+ le_sSup
+ leftLim_eq_sInf
+ map_balanceL
+ map_balanceR
+ map_eraseMax
+ map_eraseMin
+ map_findMax'
+ map_findMin'
+ map_id
+ map_map
+ map_node'
+ map_rotateL
+ map_rotateR
+ map_singleton
+ map_val_atBot_of_Iic_subset
+ measurable_ofDual
+ measurable_toDual
+ mem_dual
+ ofDual_comp_image_preimage
+ ofDual_comp_image_preimage'
+ ofDual_injective
+ ofDual_smul
+ ofDual_smul'
+ ofDual_sum'
+ ofDual_surjective
+ pred_iterate_toDual
+ rightLim_eq_sSup
+ sInf_le
+ sSup_le
+ size_map
+ succ_iterate_toDual
+ toDual_comp_image_preimage
+ toDual_injective
+ toDual_smul
+ toDual_smul'
+ toDual_surjective
+ val_toMonoidWithZeroHom_apply
++ sup
++-- dual_pure
+-+- dual_top
+-+- iInf_orthogonal
+-+- le_rightLim
+-+- rightLim
+-+- rightLim_le
+-+- sInf_orthogonal
+-+- tendsto_rightLim_within
+-+- toColex_monotone
+-+-+-+-+-+-+-+-+- symm_dual_id
+-+-+-+-+-+-+-+-+-+-+- dual_id
+-- ciInf_le
- Antitone.map_iSup_le
- Antitone.map_iSup₂_le
- BddAbove.bddBelow_image2_of_bddAbove
- BddAbove.image2_bddBelow
- BddBelow.bddBelow_image2_of_bddAbove
- BddBelow.image2
- BddBelow.range_comp
- Bounded.dual_iff
- Equiv.biInf_comp
- Equiv.iInf_comp
- Equiv.iInf_congr
- Function.Surjective.iInf_comp
- Function.Surjective.iInf_congr
- IsCoatom.Ici_eq
- IsCoatom.le_iff_eq
- IsCoatom.lt_iff
- IsCoatom.ne_top
- IsCoatom.ne_top_iff_eq
- IsCoinitialFor.image_of_antitone
- IsCoinitialFor.image_of_monotone
- IsGLB.ciInf_eq
- IsGLB.ciInf_set_eq
- IsGLB.csInf_eq
- IsGLB.iInf_eq
- IsGLB.insert
- IsGLB.unique
- IsGreatest.isGreatest_iff_eq
- IsGreatest.isLeast_image2
- IsGreatest.isLeast_image2_of_isLeast
- IsGreatest.unique
- IsLeast.csInf_eq
- IsLeast.csInf_mem
- IsLeast.image2
- IsLeast.isLeast_image2_of_isGreatest
- IsMaxFilter.comp_mono
- IsMaxFilter.comp_tendsto
- IsMaxFilter.filter_inf
- IsMaxFilter.filter_mono
- IsMaxFilter.tendsto_principal_Iic
- IsMaxOn.bddAbove
- IsMaxOn.comp_mapsTo
- IsMaxOn.comp_mono
- IsMaxOn.inter
- IsMaxOn.isLUB
- IsMaxOn.on_preimage
- IsMaxOn.on_subset
- IsMinOn.iInf_eq
- Monotone.map_iInf_le
- Monotone.map_iInf₂_le
- Ord.dual_dual
- Preorder.dual_dual
- SemilatticeInf.dual_dual
- SemilatticeSup.dual_dual
- Set.BijOn.iInf_comp
- Set.BijOn.iInf_congr
- Set.Iic_ciInf
- _root_.LinearOrder.swap
- bddBelow_pi
- bddBelow_prod
- bddBelow_range_pi
- bddBelow_range_prod
- bddBelow_u_image
- biInf_congr
- biInf_const
- biInf_inf
- biInf_le
- biInf_lt_iff
- biInf_prod
- biInf_prod'
- biSup_inf_le_biSup_inf
- biSup_inf_le_inf_biSup
- bliminf_congr
- bliminf_eq
- bliminf_eq_liminf
- bliminf_eq_liminf_subtype
- bliminf_true
- cbiInf_eq_of_forall
- ciInf_Ici
- ciInf_const
- ciInf_eq_ite
- ciInf_eq_of_forall_ge_of_forall_gt_exists_lt
- ciInf_eq_univ_of_not_bddBelow
- ciInf_le_of_le
- ciInf_lt_iff
- ciInf_neg
- ciInf_of_not_bddBelow
- ciInf_pos
- ciInf_set_le
- ciInf_subsingleton
- ciInf_subtype'
- ciInf_subtype''
- ciInf_unique
- coheight_ofDual
- csInf_eq_csInf_of_forall_exists_le
- csInf_eq_of_forall_ge_of_forall_gt_exists_lt
- csInf_eq_univ_of_not_bddBelow
- csInf_image
- csInf_insert
- csInf_le
- csInf_le_csInf
- csInf_le_iff
- csInf_le_of_le
- csInf_lt_of_lt
- csInf_of_not_bddBelow
- csInf_pair
- csInf_singleton
- csInf_union
- csInf_upperBounds_eq_csSup
- csInf_upperBounds_range
- dual_insert
- dual_ordConnectedSection
- eq_singleton_top_of_sInf_eq_top_of_nonempty
- exists_lt_of_ciInf_lt
- exists_lt_of_csInf_lt
- gfp_induction
- gfp_le
- gfp_le_map
- height_ofDual
- iInf_and
- iInf_and'
- iInf_biUnion
- iInf_bool_eq
- iInf_comm
- iInf_congr
- iInf_congr_Prop
- iInf_const
- iInf_dite
- iInf_emptyset
- iInf_eq_dif
- iInf_eq_iInf_finset
- iInf_eq_iInf_finset'
- iInf_eq_if
- iInf_eq_of_forall_ge_of_forall_gt_exists_lt
- iInf_eq_top
- iInf_exists
- iInf_extend_top
- iInf_false
- iInf_iInf_eq_left
- iInf_iInf_eq_right
- iInf_iUnion
- iInf_image
- iInf_image2
- iInf_inf
- iInf_inf_eq
- iInf_insert_update
- iInf_ite
- iInf_le
- iInf_le_iInf₂
- iInf_le_of_le
- iInf_lt_iff
- iInf_lt_top
- iInf_mono
- iInf_mono'
- iInf_nat_gt_zero_eq
- iInf_ne_top_subtype
- iInf_neg
- iInf_of_empty
- iInf_option
- iInf_option_elim
- iInf_option_toFinset
- iInf_or
- iInf_pair
- iInf_plift_down
- iInf_plift_up
- iInf_pos
- iInf_prod
- iInf_prod'
- iInf_psigma
- iInf_psigma'
- iInf_range
- iInf_range'
- iInf_sUnion
- iInf_sigma
- iInf_sigma'
- iInf_split
- iInf_split_single
- iInf_subtype
- iInf_subtype'
- iInf_subtype''
- iInf_sum
- iInf_sup_iInf_le
- iInf_top
- iInf_true
- iInf_unique
- iInf_univ
- iInf₂_comm
- iInf₂_eq_top
- iInf₂_le
- iInf₂_le_of_le
- iInf₂_mono
- iInf₂_mono'
- iSup_inf_le_iSup_inf
- iSup_inf_le_inf_iSup
- iSup_inf_le_inf_sSup
- iSup_inf_le_sSup_inf
- iUnion_Ici
- image2_lowerBounds_lowerBounds_subset
- image2_lowerBounds_lowerBounds_subset_lowerBounds_image2
- image2_lowerBounds_upperBounds_subset_lowerBounds_image2
- image2_upperBounds_lowerBounds_subset_lowerBounds_image2
- inf_biInf
- inf_eq_iInf
- inf_iInf
- instIntCast
- instLinearOrder.dual_dual
- instPartialOrder.dual_dual
- instance (priority := 10) WithTop.instLE : LE (WithTop α) where le a b := WithBot.LE (α := αᵒᵈ) b a
- instance (priority := 10) WithTop.instLT : LT (WithTop α) where lt a b := WithBot.LT (α := αᵒᵈ) b a
- instance (priority := 100) [LocallyFiniteOrder ι] [PredOrder ι] : IsPredArchimedean ι
- instance (priority := 100) normedGroup [NormedGroup E] : NormedGroup Eᵒᵈ := ‹NormedGroup E›
- instance (priority := 100) seminormedCommGroup [SeminormedCommGroup E] : SeminormedCommGroup Eᵒᵈ
- instance (priority := 90) OrderHomClass.toOrderHomClassOrderDual [LE α] [LE β]
- instance (priority := 90) OrderIsoClass.toOrderIsoClassOrderDual [LE α] [LE β]
- instance : Bornology αᵒᵈ
- instance : BoundedGENhdsClass αᵒᵈ := ⟨@isBounded_le_nhds α _ _ _⟩
- instance : BoundedLENhdsClass αᵒᵈ := ⟨@isBounded_ge_nhds α _ _ _⟩
- instance : ContinuousConstSMul M αᵒᵈ := ‹ContinuousConstSMul M α›
- instance : ContinuousInv ℝ≥0∞ := ⟨OrderIso.invENNReal.continuous⟩
- instance : ContinuousNeg EReal := ⟨negOrderIso.continuous⟩
- instance : Dist Xᵒᵈ := ‹Dist X›
- instance : EDist Xᵒᵈ := ‹EDist X›
- instance : OrderClosedTopology αᵒᵈ
- instance : PseudoMetricSpace αᵒᵈ := ‹_›
- instance : ∀ [Inhabited α], Inhabited αᵒᵈ := fun [x : Inhabited α] => x
- instance [BoundedSpace α] : BoundedSpace αᵒᵈ
- instance [EMetricSpace X] : EMetricSpace Xᵒᵈ := ‹EMetricSpace X›
- instance [LinearOrder α] : LinearOrder (Lex (NonemptyInterval α)) := fast_instance%
- instance [MetricSpace X] : MetricSpace Xᵒᵈ := ‹MetricSpace X›
- instance [Mul R] [Add R] [h : LeftDistribClass R] : LeftDistribClass Rᵒᵈ := h
- instance [Mul R] [Add R] [h : RightDistribClass R] : RightDistribClass Rᵒᵈ := h
- instance [Mul R] [h : HasDistribNeg R] : HasDistribNeg Rᵒᵈ := h
- instance [Mul α] [Zero α] [h : IsCancelMulZero α] : IsCancelMulZero αᵒᵈ := h
- instance [Mul α] [Zero α] [h : IsLeftCancelMulZero α] : IsLeftCancelMulZero αᵒᵈ := h
- instance [Mul α] [Zero α] [h : IsRightCancelMulZero α] : IsRightCancelMulZero αᵒᵈ := h
- instance [Mul α] [Zero α] [h : NoZeroDivisors α] : NoZeroDivisors αᵒᵈ := h
- instance [Mul α] [h : IsCancelMul α] : IsCancelMul αᵒᵈ := h
- instance [Mul α] [h : IsLeftCancelMul α] : IsLeftCancelMul αᵒᵈ := h
- instance [Mul α] [h : IsRightCancelMul α] : IsRightCancelMul αᵒᵈ := h
- instance [PseudoEMetricSpace X] : PseudoEMetricSpace Xᵒᵈ := ‹PseudoEMetricSpace X›
- instance [PseudoMetricSpace X] [ProperSpace X] : ProperSpace Xᵒᵈ := ‹ProperSpace X›
- instance [Ring R] [h : IsDomain R] : IsDomain Rᵒᵈ := h
- instance [TopologicalSpace α] [h : FirstCountableTopology α] : FirstCountableTopology αᵒᵈ := h
- instance [TopologicalSpace α] [h : SecondCountableTopology α] : SecondCountableTopology αᵒᵈ := h
- instance [TopologicalSpace α] [h : SeparableSpace α] : SeparableSpace αᵒᵈ := h
- instance [h : CancelMonoid α] : CancelMonoid αᵒᵈ := h
- instance [h : CommGroup α] : CommGroup αᵒᵈ := h
- instance [h : CommGroupWithZero α] : CommGroupWithZero αᵒᵈ := h
- instance [h : CommMonoidWithZero α] : CommMonoidWithZero αᵒᵈ := h
- instance [h : CommRing R] : CommRing Rᵒᵈ := h
- instance [h : CommSemigroup α] : CommSemigroup αᵒᵈ := h
- instance [h : CommSemiring R] : CommSemiring Rᵒᵈ := h
- instance [h : Distrib R] : Distrib Rᵒᵈ := h
- instance [h : Div α] : Div αᵒᵈ := h
- instance [h : DivInvMonoid α] : DivInvMonoid αᵒᵈ := h
- instance [h : DivisionCommMonoid α] : DivisionCommMonoid αᵒᵈ := h
- instance [h : DivisionMonoid α] : DivisionMonoid αᵒᵈ := h
- instance [h : GroupWithZero α] : GroupWithZero αᵒᵈ := h
- instance [h : Inv α] : Inv αᵒᵈ := h
- instance [h : InvolutiveInv α] : InvolutiveInv αᵒᵈ := h
- instance [h : LeftCancelMonoid α] : LeftCancelMonoid αᵒᵈ := h
- instance [h : LeftCancelSemigroup α] : LeftCancelSemigroup αᵒᵈ := h
- instance [h : MeasurableSpace α] : MeasurableSpace αᵒᵈ := h
- instance [h : Monoid α] : Monoid αᵒᵈ := h
- instance [h : MonoidWithZero α] : MonoidWithZero αᵒᵈ := h
- instance [h : Mul α] : Mul αᵒᵈ := h
- instance [h : MulOneClass α] : MulOneClass αᵒᵈ := h
- instance [h : MulZeroClass α] : MulZeroClass αᵒᵈ := h
- instance [h : MulZeroOneClass α] : MulZeroOneClass αᵒᵈ := h
- instance [h : NonAssocRing R] : NonAssocRing Rᵒᵈ := h
- instance [h : NonAssocSemiring R] : NonAssocSemiring Rᵒᵈ := h
- instance [h : NonUnitalCommRing R] : NonUnitalCommRing Rᵒᵈ := h
- instance [h : NonUnitalCommSemiring R] : NonUnitalCommSemiring Rᵒᵈ := h
- instance [h : NonUnitalNonAssocRing R] : NonUnitalNonAssocRing Rᵒᵈ := h
- instance [h : NonUnitalNonAssocSemiring R] : NonUnitalNonAssocSemiring Rᵒᵈ := h
- instance [h : NonUnitalRing R] : NonUnitalRing Rᵒᵈ := h
- instance [h : NonUnitalSemiring R] : NonUnitalSemiring Rᵒᵈ := h
- instance [h : Nontrivial α] : Nontrivial αᵒᵈ := h
- instance [h : One α] : One αᵒᵈ := h
- instance [h : RightCancelMonoid α] : RightCancelMonoid αᵒᵈ := h
- instance [h : RightCancelSemigroup α] : RightCancelSemigroup αᵒᵈ := h
- instance [h : Ring R] : Ring Rᵒᵈ := h
- instance [h : Semigroup α] : Semigroup αᵒᵈ := h
- instance [h : SemigroupWithZero α] : SemigroupWithZero αᵒᵈ := h
- instance [h : Semiring R] : Semiring Rᵒᵈ := h
- instance [h : Unique α] : Unique αᵒᵈ := h
- instance [t : OrderTopology α] : OrderTopology αᵒᵈ
- isFixedPt_gfp
- isGLB_biInf
- isGLB_ciInf
- isGLB_ciInf_set
- isGLB_csInf
- isGLB_iInf
- isGLB_pair
- isGLB_pi
- isGLB_prod
- isGLB_u_image
- isGreatest_gfp
- isGreatest_gfp_le
- isGreatest_u
- isLUB_u
- isMaxFilter_const
- isMaxOn_const
- isMaxOn_iff
- isMaxOn_univ_iff
- le_ciInf
- le_ciInf_iff
- le_ciInf_set_iff
- le_csInf
- le_csInf_iff
- le_csInf_inter
- le_gfp
- le_iInf
- le_iInf_comp
- le_iInf_const
- le_iInf_iff
- le_iInf₂
- le_iInf₂_iff
- le_sInf_inter
- liminf_comp
- liminf_congr
- liminf_eq
- liminf_nat_add
- lowerBounds_u_image
- lt_iInf_iff
- map_gfp
- map_le_gfp
- mem_lowerBounds_image2
- mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds
- mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds
- mem_lowerBounds_image2_of_mem_upperBounds
- notMem_of_csSup_lt
- ofDual
- ofDual_ofNat
- ofDual_symm_eq
- ofDual_trans_toDual
- rec
- sInf_diff_singleton_top
- sInf_eq_iInf
- sInf_eq_iInf'
- sInf_eq_of_forall_ge_of_forall_gt_exists_lt
- sInf_iUnion_Ici
- sInf_image
- sInf_image'
- sInf_image2
- sInf_insert
- sInf_le_sInf_of_subset_insert_top
- sInf_pair
- sInf_range
- sInf_sUnion
- sInf_union
- sInf_upperBounds_eq_sSup
- toDual
- toDual_ofNat
- toDual_symm_eq
- toDual_trans_ofDual
- u_iInf
- u_iInf₂
- u_inf
- u_sInf
-++- ext
-++--- map_isGreatest
-- iInf_insert
-- iInf_singleton
-- iInf_union
-- image_lowerBounds_subset_lowerBounds_image
-- image_upperBounds_subset_lowerBounds_image
-- map_isLeast
-- mem_lowerBounds_image_self
--- this
---- map_bddBelow
---- mem_lowerBounds_image
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
Decrease in tech debt: (relative, absolute) = (0.29, 0.00)
| Current number | Change | Type |
|---|---|---|
| 492 | -2 | porting notes |
| 1364 | 5 | backwards compatibility flags |
| 1349 | 5 | privateInPublic flags |
| 626 | -3 | erw |
Current commit a51cf56997
Reference commit ae6b7e9128
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
Adapt 22 files across Order, Category, Filter, Algebra, LinearAlgebra, and Combinatorics to the new OrderDual one-field structure definition. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Adapt 9 more files to the OrderDual structure change: - Convex/Basic, Chebyshev: direct proofs instead of βᵒᵈ delegation - DFinsupp/Lex: direct Colex instances instead of ιᵒᵈ delegation - Topology/Order: GC/GCI lemma unwrapping with toDual/ofDual - Bornology/Basic: explicit Bornology αᵒᵈ via Filter.map toDual - MinimalPrime: Zorn proof with explicit ofDual/toDual - Noetherian/Defs: WellFoundedGT via InvImage.wf - ArchimedeanDensely: OrderDual.equiv ℤ - FinBoolAlg: dualDual symm direction Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Adapt Filter IsBounded, Ultrafilter, and CountablyGenerated to the OrderDual structure change. Direct proofs for IsBounded dual lemmas, comap-based proofs for CountablyGenerated OrderDual instances. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Adapt AddValuation to work with OrderDual as a structure. Key changes: - New FunLike instance for AddValuation using ofDual/toAdd - val_toMonoidWithZeroHom_apply helper lemma - Rewrite delegate lemmas (map_zero, map_one, map_mul, etc.) through val_toMonoidWithZeroHom_apply - Fix IsEquiv.map injection proof - Fix mem_supp_iff and map_add_supp Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Adapt LiminfLimsup, Topology/Constructions, Convex/Function, Finsupp/Lex, DFinsupp/WellFounded, Noetherian/Basic, Valuation/ValuationSubring, Valuation/Quotient, Torsion/Basic, Bornology/Constructions, and Convex/Combination to the new OrderDual structure. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Adapt Jensen, Finsupp/WellFounded, Dual/Lemmas, Localization/Submodule, Spectrum/Prime/Basic, and NhdsWithin to the new OrderDual structure. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
github-actions
bot
added
the
merge-conflict
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Fix 68 errors across 6 files: - IsLUB.lean: rewrite GLB theorems with direct proofs - MonotoneContinuity.lean: rewrite left-continuity theorems directly - UpperLowerSetTopology.lean: fix OrderDual instances and lambdas - HullKernel.lean: fix toDual/ofDual wrapping - Group/Basic.lean: fix ContinuousInv instance for OrderDual - KrullsHeightTheorem.lean: fix OrderHom construction Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…structure Fix 61 errors across 7 files: - Monotone.lean: rewrite all dual delegations with direct proofs - DenselyOrdered.lean: direct proofs for closure_Iio', interior_Iic' - UpperLower.lean: fix HasUpperLowerClosure instance for OrderDual - AtTopBotIxx.lean: direct proofs for nhdsGT/atBot variants - LinearUpperLowerSetTopology.lean: direct CompletelyNormalSpace proof - Galois/Infinite.lean: fix IntermediateFieldEquivClosedSubgroup - IdealSheaf/Basic.lean: fix GaloisConnection and support lemmas Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…ange Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…hange Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…l structure change Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…derDual instances Move `ofDual_injective`, `toDual_injective`, `ofDual_surjective`, `toDual_surjective` to `Order/Synonym.lean` where they logically belong. Remove duplicates from `Algebra/Field/Basic.lean` and `Topology/Bornology/Basic.lean`. Fix OrderDual instances for `MeasurableSup₂`/`MeasurableInf₂`, `OpensMeasurableSpace`, and `BorelSpace`. Fix `AntitoneOn.countable_not_continuousWithinAt` proof. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…x warnings - Remove unprovable `dual_ordConnectedSection` (relied on `Classical.choose` giving the same value on `αᵒᵈ` vs `α`, which no longer holds with OrderDual as a structure). Rewrite the T5 proof to avoid it. - Adapt `BorelSpace/Order.lean` to the OrderDual structure change. - Fix linter warnings across multiple files: unused variables, flexible simp, `show` vs `change`, line length, simp-before-to_additive. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
# Conflicts: # Mathlib/Order/Filter/AtTopBot/Defs.lean
github-actions
bot
removed
the
merge-conflict
…ture change - EssSup.lean: Write direct proofs for `essInf_measure_zero`, `le_essInf_of_ae_le`, and `OrderIso.essInf_apply` instead of delegating to `essSup` on `βᵒᵈ` (which gives results in a different type now) - Polish/Basic.lean: Fix `image_of_antitoneOn` by unfolding `MeasurableSet` on `αᵒᵈ` and using `preimage_image_eq` with `toDual_injective` - AEEqOfLIntegral.lean: Fix `ae_le_const_iff_forall_gt_measure_zero` by explicitly converting the dual quantifier using `OrderDual.forall` simp lemma Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Write direct proof for `integrableAtFilter_atTop_iff` instead of delegating to `integrableAtFilter_atBot_iff (α := αᵒᵈ)`. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…to OrderDual structure change Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
- Remove @[simp] from ofDual_toDual (simpVarHead: LHS is a variable) - Remove @[simp] from toDual_inj (subsumed by toDual.injEq) - Add docstring to OrderDual.homeomorph - Change @[simps!] to @[simps] on sSupHom.dual and CompleteLatticeHom.dual (generated lemma LHS simplified via toFun_eq_coe) - Remove unused autoParam args from OrderIso.liminf_apply Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Replace manually-written dual theorems with @[to_dual]-generated ones across CompleteLattice, Bounds, Atoms, GaloisConnection, FixedPoints, Set.Lattice, Interval, and Finset files (-531 net lines). Also fix named argument b₁/b₂ → a₁/a₂ in callers of GaloisConnection.u_inf, which is now auto-generated from l_sup (which uses a₁/a₂) rather than manually defined (which used b₁/b₂). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
kim-em
force-pushed
the
kim/move-OrderDual
branch
from
268ac51 to
955e0a6
Compare
Register `ConditionallyCompleteLattice` and `ConditionallyCompleteLinearOrder` class field projections with `@[to_dual existing]` in Defs.lean, then tag ~30 theorem pairs in Basic.lean and Indexed.lean with `@[to_dual]` to auto-generate their duals, replacing manual versions. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Register all remaining dual theorem pairs across CCL files: - Basic.lean: auto-generate 6 duals, register 2 existing pairs (-45 net lines) - Indexed.lean: register 21 pairs for downstream @[to_dual] usage - Group.lean: register 4 multiplicative dual pairs - Finset.lean: register 10 pairs (max'/min'/sup'/inf' blocked by missing registrations) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…ate duals Convert ~30 manual dual theorem pairs to @[to_dual] auto-generation, deleting the manually written duals. Also add nameDict entries for limsup/liminf and definition registrations for LiminfLimsup.lean. - Indexed.lean: 15 pairs converted (-91 lines) - Extr.lean: 14 pairs converted (-65 lines) - ToDual.lean: 4 nameDict entries for limsup/liminf family - LiminfLimsup.lean: 3 definition registrations added Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…l theorems Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
mathlib-merge-conflicts
bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
1 participant
This PR changes
OrderDualfrom a type alias (def OrderDual (α : Type*) := α) to a one-field structure:This prevents defeq abuse between
αandαᵒᵈ, requiring explicittoDual/ofDualwrapping at type boundaries.🤖 Prepared with Claude Code