Commit 2023-01-23 20:17 c708b1d3

View on Github →

feat: port Order.Filter.Extr (#1785) This mighta been the easiest port so far. Just a couple translation errors. Only weird thing is that it was not able to infer what a ConditionallyCompleteLinearOrder was, so I added import Mathlib.Order.ConditionallyCompleteLattice.Basic. Is that legal?

Estimated changes

added theorem IsExtrFilter.comp_mono
added theorem IsExtrFilter.congr
added theorem IsExtrFilter.neg
added def IsExtrFilter
added theorem IsExtrOn.comp_antitone
added theorem IsExtrOn.comp_mapsTo
added theorem IsExtrOn.comp_mono
added theorem IsExtrOn.elim
added theorem IsExtrOn.inter
added theorem IsExtrOn.neg
added theorem IsExtrOn.on_preimage
added theorem IsExtrOn.on_subset
added def IsExtrOn
added theorem IsMaxFilter.add
added theorem IsMaxFilter.comp_mono
added theorem IsMaxFilter.congr
added theorem IsMaxFilter.filter_inf
added theorem IsMaxFilter.inf
added theorem IsMaxFilter.isExtr
added theorem IsMaxFilter.max
added theorem IsMaxFilter.min
added theorem IsMaxFilter.neg
added theorem IsMaxFilter.sub
added theorem IsMaxFilter.sup
added def IsMaxFilter
added theorem IsMaxOn.add
added theorem IsMaxOn.bicomp_mono
added theorem IsMaxOn.comp_antitone
added theorem IsMaxOn.comp_mapsTo
added theorem IsMaxOn.comp_mono
added theorem IsMaxOn.inf
added theorem IsMaxOn.inter
added theorem IsMaxOn.isExtr
added theorem IsMaxOn.max
added theorem IsMaxOn.min
added theorem IsMaxOn.neg
added theorem IsMaxOn.on_preimage
added theorem IsMaxOn.on_subset
added theorem IsMaxOn.sub
added theorem IsMaxOn.sup
added theorem IsMaxOn.supᵢ_eq
added def IsMaxOn
added theorem IsMinFilter.add
added theorem IsMinFilter.comp_mono
added theorem IsMinFilter.congr
added theorem IsMinFilter.filter_inf
added theorem IsMinFilter.inf
added theorem IsMinFilter.isExtr
added theorem IsMinFilter.max
added theorem IsMinFilter.min
added theorem IsMinFilter.neg
added theorem IsMinFilter.sub
added theorem IsMinFilter.sup
added def IsMinFilter
added theorem IsMinOn.add
added theorem IsMinOn.bicomp_mono
added theorem IsMinOn.comp_antitone
added theorem IsMinOn.comp_mapsTo
added theorem IsMinOn.comp_mono
added theorem IsMinOn.inf
added theorem IsMinOn.infᵢ_eq
added theorem IsMinOn.inter
added theorem IsMinOn.isExtr
added theorem IsMinOn.max
added theorem IsMinOn.min
added theorem IsMinOn.neg
added theorem IsMinOn.on_preimage
added theorem IsMinOn.on_subset
added theorem IsMinOn.sub
added theorem IsMinOn.sup
added def IsMinOn
added theorem isExtrFilter_const
added theorem isExtrFilter_dual_iff
added theorem isExtrOn_const
added theorem isExtrOn_dual_iff
added theorem isMaxFilter_const
added theorem isMaxFilter_dual_iff
added theorem isMaxOn_const
added theorem isMaxOn_dual_iff
added theorem isMaxOn_iff
added theorem isMaxOn_univ_iff
added theorem isMinFilter_const
added theorem isMinFilter_dual_iff
added theorem isMinOn_const
added theorem isMinOn_dual_iff
added theorem isMinOn_iff
added theorem isMinOn_univ_iff