Commit 2023-01-25 09:27 9a750ff3

View on Github →

feat: port Order.PartialSups (#1757) port of order.partial.sups

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Tropical/BigOperators.lean

Modified Mathlib/Data/Set/Finite.lean

deleted theorem Set.Finite.infᵢ_bsupr_of_antitone

deleted theorem Set.Finite.infᵢ_bsupr_of_monotone

added theorem Set.Finite.infᵢ_bsupᵢ_of_antitone

added theorem Set.Finite.infᵢ_bsupᵢ_of_monotone

Modified Mathlib/Order/ConditionallyCompleteLattice/Finset.lean

deleted theorem Finset.inf'_eq_cInf_image

added theorem Finset.inf'_eq_cinfₛ_image

deleted theorem Finset.inf'_id_eq_cInf

added theorem Finset.inf'_id_eq_cinfₛ

deleted theorem Finset.sup'_eq_cSup_image

added theorem Finset.sup'_eq_csupₛ_image

deleted theorem Finset.sup'_id_eq_cSup

added theorem Finset.sup'_id_eq_csupₛ

Created Mathlib/Order/PartialSups.lean

added theorem Monotone.partialSups_eq

added theorem bddAbove_range_partialSups

added theorem csupᵢ_partialSups_eq

added theorem le_partialSups

added theorem le_partialSups_of_le

added def partialSups.gi

added def partialSups

added theorem partialSups_disjoint_of_disjoint

added theorem partialSups_eq_bsupᵢ

added theorem partialSups_eq_csupᵢ_Iic

added theorem partialSups_eq_sup'_range

added theorem partialSups_eq_sup_range

added theorem partialSups_le

added theorem partialSups_mono

added theorem partialSups_succ

added theorem partialSups_zero

added theorem supᵢ_eq_supᵢ_of_partialSups_eq_partialSups

added theorem supᵢ_le_supᵢ_of_partialSups_le_partialSups

added theorem supᵢ_partialSups_eq