Commit 2024-11-08 16:20 94ba4cbb

View on Github →

chore: unify binary inf and min (#18707) Unify binary inf and min, as discussed in https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60sup.60.2F.60inf.60.20or.20.60max.60.2F.60min.60.20for.20set.20interval.20lemmas.3F.

Estimated changes

modified def BooleanRing.inf
modified def BooleanRing.sup
deleted theorem ENNReal.sup_eq_max
modified theorem Finset.inf_eq_inter
modified theorem Finset.sup_eq_union
modified theorem Bool.inf_eq_band
modified theorem Bool.sup_eq_bor
modified theorem Filter.EventuallyEq.inf
modified theorem Filter.EventuallyEq.sup
modified theorem Filter.Germ.const_inf
modified theorem Filter.Germ.const_sup
modified structure InfHom
modified structure InfTopHom
modified structure SupBotHom
modified structure SupHom
modified def Lattice.mk'
modified theorem Pi.inf_apply
modified theorem Pi.inf_def
modified theorem Pi.sup_apply
modified theorem Pi.sup_def
modified theorem Prod.fst_inf
modified theorem Prod.fst_sup
modified theorem Prod.inf_def
modified theorem Prod.mk_inf_mk
modified theorem Prod.mk_sup_mk
modified theorem Prod.snd_inf
modified theorem Prod.snd_sup
modified theorem Prod.sup_def
modified theorem Prod.swap_inf
modified theorem Prod.swap_sup
modified def SemilatticeInf.mk'
modified def SemilatticeSup.mk'
deleted theorem inf_eq_min
modified theorem ofDual_inf
modified theorem ofDual_sup
deleted theorem sup_eq_max
modified theorem toDual_inf
modified theorem toDual_sup
modified theorem max_le_max_left
modified theorem max_le_max_right
modified theorem min_le_min_left
modified theorem min_le_min_right
modified def bihimp
modified theorem bihimp_def
modified def symmDiff
modified theorem symmDiff_def
modified theorem ULift.down_inf
modified theorem ULift.down_sup
modified theorem ULift.up_inf
modified theorem ULift.up_sup
modified theorem Continuous.inf
modified theorem Continuous.sup
modified theorem Filter.Tendsto.inf_nhds'
modified theorem Filter.Tendsto.inf_nhds
modified theorem Filter.Tendsto.sup_nhds'
modified theorem Filter.Tendsto.sup_nhds
modified theorem continuous_inf
modified theorem continuous_sup