Commit 2024-04-23 01:17 16e2255a

View on Github →

fix: generalize index types of iSup to Sort (#12114) This breaks a few simp proofs which were expecting these lemmas to apply to the data binders but not the prop binders.

Estimated changes

Modified Mathlib/Algebra/Lie/Submodule.lean

modified theorem LieSubmodule.iSup_eq_top_iff_coe_toSubmodule

Modified Mathlib/Algebra/Module/Torsion.lean

Modified Mathlib/Analysis/LocallyConvex/Barrelled.lean

modified theorem Seminorm.continuous_iSup

Modified Mathlib/Analysis/Seminorm.lean

modified theorem Seminorm.bddAbove_of_absorbent

modified theorem Seminorm.closedBall_iSup

Modified Mathlib/FieldTheory/Adjoin.lean

Modified Mathlib/FieldTheory/PurelyInseparable.lean

Modified Mathlib/LinearAlgebra/Dual.lean

modified theorem Submodule.dualAnnihilator_iSup_eq

modified theorem Submodule.dualCoannihilator_iSup_eq

modified theorem Submodule.iSup_dualAnnihilator_le_iInf

Modified Mathlib/LinearAlgebra/LinearIndependent.lean

Modified Mathlib/LinearAlgebra/Span.lean

modified theorem LinearMap.ext_on_range

modified theorem Submodule.span_range_eq_iSup

Modified Mathlib/Order/Filter/Basic.lean

added theorem Filter.iInf_principal'

modified theorem Filter.iInf_principal

Modified Mathlib/RingTheory/Finiteness.lean

modified theorem Submodule.fg_iSup

Modified Mathlib/Topology/Order.lean