Skip to content

Commit 21f6296

Browse files
mattrobballmattrobball
committed
Merge branch 'master' into port/CategoryTheory.Limits.HasLimits
2 parents 1985f48 + 5107462 commit 21f6296

File tree

22 files changed

+4847
-97
lines changed

22 files changed

+4847
-97
lines changed

‎Mathlib.lean‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -251,6 +251,7 @@ import Mathlib.CategoryTheory.EqToHom
251251
import Mathlib.CategoryTheory.Equivalence
252252
import Mathlib.CategoryTheory.EssentialImage
253253
import Mathlib.CategoryTheory.EssentiallySmall
254+
import Mathlib.CategoryTheory.Filtered
254255
import Mathlib.CategoryTheory.FinCategory
255256
import Mathlib.CategoryTheory.FullSubcategory
256257
import Mathlib.CategoryTheory.Functor.Basic
@@ -276,6 +277,7 @@ import Mathlib.CategoryTheory.Limits.IsLimit
276277
import Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
277278
import Mathlib.CategoryTheory.Monoidal.Category
278279
import Mathlib.CategoryTheory.Monoidal.Functor
280+
import Mathlib.CategoryTheory.Monoidal.Functorial
279281
import Mathlib.CategoryTheory.NatIso
280282
import Mathlib.CategoryTheory.NatTrans
281283
import Mathlib.CategoryTheory.Opposites
@@ -320,6 +322,7 @@ import Mathlib.Combinatorics.SetFamily.LYM
320322
import Mathlib.Combinatorics.SetFamily.Shadow
321323
import Mathlib.Combinatorics.SimpleGraph.Basic
322324
import Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
325+
import Mathlib.Combinatorics.SimpleGraph.Subgraph
323326
import Mathlib.Combinatorics.Young.SemistandardTableau
324327
import Mathlib.Combinatorics.Young.YoungDiagram
325328
import Mathlib.Computability.DFA
@@ -648,6 +651,7 @@ import Mathlib.Data.Rat.Sqrt
648651
import Mathlib.Data.Real.Basic
649652
import Mathlib.Data.Real.CauSeq
650653
import Mathlib.Data.Real.CauSeqCompletion
654+
import Mathlib.Data.Real.ENNReal
651655
import Mathlib.Data.Real.NNReal
652656
import Mathlib.Data.Real.Pointwise
653657
import Mathlib.Data.Real.Sign
@@ -948,6 +952,7 @@ import Mathlib.Order.Filter.Basic
948952
import Mathlib.Order.Filter.Cofinite
949953
import Mathlib.Order.Filter.CountableInter
950954
import Mathlib.Order.Filter.Curry
955+
import Mathlib.Order.Filter.ENNReal
951956
import Mathlib.Order.Filter.Extr
952957
import Mathlib.Order.Filter.FilterProduct
953958
import Mathlib.Order.Filter.Germ

‎Mathlib/Algebra/BigOperators/Multiset/Lemmas.lean‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,13 @@ theorem prod_eq_one_iff [CanonicallyOrderedMonoid α] {m : Multiset α} :
3131

3232
end Multiset
3333

34+
@[simp]
35+
lemma CanonicallyOrderedCommSemiring.multiset_prod_pos {R} [CanonicallyOrderedCommSemiring R]
36+
[Nontrivial R] {m : Multiset R} : 0 < m.prod ↔ (∀ x ∈ m, (0 : R) < x) := by
37+
rcases m with ⟨l⟩
38+
rw [Multiset.quot_mk_to_coe'', Multiset.coe_prod]
39+
exact CanonicallyOrderedCommSemiring.list_prod_pos
40+
3441
open Multiset
3542

3643
namespace Commute

‎Mathlib/Algebra/BigOperators/Order.lean‎

Lines changed: 23 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Johannes Hölzl
55
66
! This file was ported from Lean 3 source module algebra.big_operators.order
7-
! leanprover-community/mathlib commit 509de852e1de55e1efa8eacfa11df0823f26f226
7+
! leanprover-community/mathlib commit afdb4fa3b32d41106a4a09b371ce549ad7958abd
88
! Please do not edit these lines, except to modify the commit id
99
! if you have ported upstream changes.
1010
-/
@@ -637,6 +637,12 @@ section CanonicallyOrderedCommSemiring
637637

638638
variable [CanonicallyOrderedCommSemiring R] {f g h : ι → R} {s : Finset ι} {i : ι}
639639

640+
/-- Note that the name is to match `CanonicallyOrderedCommSemiring.mul_pos`. -/
641+
@[simp] lemma _root_.CanonicallyOrderedCommSemiring.prod_pos [Nontrivial R] :
642+
0 < ∏ i in s, f i ↔ (∀ i ∈ s, (0 : R) < f i) :=
643+
CanonicallyOrderedCommSemiring.multiset_prod_pos.trans Multiset.forall_mem_map_iff
644+
#align canonically_ordered_comm_semiring.prod_pos CanonicallyOrderedCommSemiring.prod_pos
645+
640646
theorem prod_le_prod' (h : ∀ i ∈ s, f i ≤ g i) : (∏ i in s, f i) ≤ ∏ i in s, g i := by
641647
classical
642648
induction' s using Finset.induction with a s has ih h
@@ -696,49 +702,39 @@ namespace WithTop
696702
open Finset
697703

698704
/-- A product of finite numbers is still finite -/
699-
theorem prod_lt_top [CanonicallyOrderedCommSemiring R] [Nontrivial R] [DecidableEq R] {s : Finset ι}
700-
{f : ι → WithTop R} (h : ∀ i ∈ s, f i ≠ ⊤) : (∏ i in s, f i) < ⊤ :=
701-
prod_induction f (fun a ↦ a < ⊤) (fun _ _ h₁ h₂ ↦ mul_lt_top h₁.ne h₂.ne) (coe_lt_top 1)
702-
fun a ha ↦ lt_top_iff_ne_top.2 (h a ha)
705+
theorem prod_lt_top [CommMonoidWithZero R] [NoZeroDivisors R] [Nontrivial R] [DecidableEq R] [LT R]
706+
{s : Finset ι} {f : ι → WithTop R} (h : ∀ i ∈ s, f i ≠ ⊤) : (∏ i in s, f i) < ⊤ :=
707+
prod_induction f (fun a ↦ a < ⊤) (fun _ _ h₁ h₂ ↦ mul_lt_top' h₁ h₂) (coe_lt_top 1)
708+
fun a ha ↦ WithTop.lt_top_iff_ne_top.2 (h a ha)
703709
#align with_top.prod_lt_top WithTop.prod_lt_top
704710

705-
/-- A sum of finite numbers is still finite -/
706-
theorem sum_lt_top [OrderedAddCommMonoid M] {s : Finset ι} {f : ι → WithTop M}
707-
(h : ∀ i ∈ s, f i ≠ ⊤) : (∑ i in s, f i) < ⊤ :=
708-
sum_induction f (fun a ↦ a < ⊤) (fun _ _ h₁ h₂ ↦ add_lt_top.2 ⟨h₁, h₂⟩) zero_lt_top fun i hi ↦
709-
lt_top_iff_ne_top.2 (h i hi)
710-
#align with_top.sum_lt_top WithTop.sum_lt_top
711-
712711
/-- A sum of numbers is infinite iff one of them is infinite -/
713-
theorem sum_eq_top_iff [OrderedAddCommMonoid M] {s : Finset ι} {f : ι → WithTop M} :
712+
theorem sum_eq_top_iff [AddCommMonoid M] {s : Finset ι} {f : ι → WithTop M} :
714713
(∑ i in s, f i) = ⊤ ↔ ∃ i ∈ s, f i = ⊤ := by
715-
classical
716-
constructor
717-
· contrapose!
718-
exact fun h ↦ (sum_lt_top fun i hi ↦ h i hi).ne
719-
· rintro ⟨i, his, hi⟩
720-
rw [sum_eq_add_sum_diff_singleton his, hi, top_add]
714+
induction s using Finset.cons_induction <;> simp [*]
721715
#align with_top.sum_eq_top_iff WithTop.sum_eq_top_iff
722716

723717
/-- A sum of finite numbers is still finite -/
724-
theorem sum_lt_top_iff [OrderedAddCommMonoid M] {s : Finset ι} {f : ι → WithTop M} :
718+
theorem sum_lt_top_iff [AddCommMonoid M] [LT M] {s : Finset ι} {f : ι → WithTop M} :
725719
(∑ i in s, f i) < ⊤ ↔ ∀ i ∈ s, f i < ⊤ := by
726-
simp only [lt_top_iff_ne_top, ne_eq, sum_eq_top_iff, not_exists, not_and]
720+
simp only [WithTop.lt_top_iff_ne_top, ne_eq, sum_eq_top_iff, not_exists, not_and]
727721
#align with_top.sum_lt_top_iff WithTop.sum_lt_top_iff
728722

723+
/-- A sum of finite numbers is still finite -/
724+
theorem sum_lt_top [AddCommMonoid M] [LT M] {s : Finset ι} {f : ι → WithTop M}
725+
(h : ∀ i ∈ s, f i ≠ ⊤) : (∑ i in s, f i) < ⊤ :=
726+
sum_lt_top_iff.2 fun i hi => WithTop.lt_top_iff_ne_top.2 (h i hi)
727+
#align with_top.sum_lt_top WithTop.sum_lt_top
728+
729729
end WithTop
730730

731731
section AbsoluteValue
732732

733733
variable {S : Type _}
734734

735735
theorem AbsoluteValue.sum_le [Semiring R] [OrderedSemiring S] (abv : AbsoluteValue R S)
736-
(s : Finset ι) (f : ι → R) : abv (∑ i in s, f i) ≤ ∑ i in s, abv (f i) := by
737-
letI := Classical.decEq ι
738-
refine' Finset.induction_on s _ fun i s hi ih ↦ _
739-
· simp
740-
· simp only [Finset.sum_insert hi]
741-
exact (abv.add_le _ _).trans (add_le_add le_rfl ih)
736+
(s : Finset ι) (f : ι → R) : abv (∑ i in s, f i) ≤ ∑ i in s, abv (f i) :=
737+
Finset.le_sum_of_subadditive abv (map_zero _) abv.add_le _ _
742738
#align absolute_value.sum_le AbsoluteValue.sum_le
743739

744740
theorem IsAbsoluteValue.abv_sum [Semiring R] [OrderedSemiring S] (abv : R → S) [IsAbsoluteValue abv]

‎Mathlib/Algebra/Order/Monoid/WithTop.lean‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
55
Ported by: Jon Eugster
66
77
! This file was ported from Lean 3 source module algebra.order.monoid.with_top
8-
! leanprover-community/mathlib commit e7e2ba8aa216a5833b5ed85a93317263711a36b5
8+
! leanprover-community/mathlib commit afdb4fa3b32d41106a4a09b371ce549ad7958abd
99
! Please do not edit these lines, except to modify the commit id
1010
! if you have ported upstream changes.
1111
-/
@@ -146,8 +146,8 @@ theorem add_ne_top : a + b ≠ ⊤ ↔ a ≠ ⊤ ∧ b ≠ ⊤ :=
146146
add_eq_top.not.trans not_or
147147
#align with_top.add_ne_top WithTop.add_ne_top
148148

149-
theorem add_lt_top [PartialOrder α] {a b : WithTop α} : a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤ := by
150-
simp_rw [lt_top_iff_ne_top, add_ne_top]
149+
theorem add_lt_top [LT α] {a b : WithTop α} : a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤ := by
150+
simp_rw [WithTop.lt_top_iff_ne_top, add_ne_top]
151151
#align with_top.add_lt_top WithTop.add_lt_top
152152

153153
theorem add_eq_coe :
@@ -569,7 +569,7 @@ theorem add_ne_bot : a + b ≠ ⊥ ↔ a ≠ ⊥ ∧ b ≠ ⊥ :=
569569
WithTop.add_ne_top
570570
#align with_bot.add_ne_bot WithBot.add_ne_bot
571571

572-
theorem bot_lt_add [PartialOrder α] {a b : WithBot α} : ⊥ < a + b ↔ ⊥ < a ∧ ⊥ < b :=
572+
theorem bot_lt_add [LT α] {a b : WithBot α} : ⊥ < a + b ↔ ⊥ < a ∧ ⊥ < b :=
573573
@WithTop.add_lt_top αᵒᵈ _ _ _ _
574574
#align with_bot.bot_lt_add WithBot.bot_lt_add
575575

‎Mathlib/Algebra/Order/Ring/WithTop.lean‎

Lines changed: 42 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2016 Jeremy Avigad. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
55
! This file was ported from Lean 3 source module algebra.order.ring.with_top
6-
! leanprover-community/mathlib commit e7e2ba8aa216a5833b5ed85a93317263711a36b5
6+
! leanprover-community/mathlib commit afdb4fa3b32d41106a4a09b371ce549ad7958abd
77
! Please do not edit these lines, except to modify the commit id
88
! if you have ported upstream changes.
99
-/
@@ -48,14 +48,36 @@ theorem mul_def {a b : WithTop α} :
4848
theorem top_mul_top : (⊤ * ⊤ : WithTop α) = ⊤ := by simp [mul_def]; rfl
4949
#align with_top.top_mul_top WithTop.top_mul_top
5050

51-
@[simp]
52-
theorem mul_top {a : WithTop α} (h : a ≠ 0) : a * ⊤ = ⊤ := by cases a <;> simp [mul_def, h] <;> rfl
51+
theorem mul_top' (a : WithTop α) : a * ⊤ = if a = 0 then 0 else ⊤ := by
52+
induction a using recTopCoe <;> simp [mul_def] <;> rfl
53+
#align with_top.mul_top' WithTop.mul_top'
54+
55+
@[simp] theorem mul_top {a : WithTop α} (h : a ≠ 0) : a * ⊤ = ⊤ := by rw [mul_top', if_neg h]
5356
#align with_top.mul_top WithTop.mul_top
5457

55-
@[simp]
56-
theorem top_mul {a : WithTop α} (h : a ≠ 0) : ⊤ * a = ⊤ := by cases a <;> simp [mul_def, h] <;> rfl
58+
theorem top_mul' (a : WithTop α) : ⊤ * a = if a = 0 then 0 else ⊤ := by
59+
induction a using recTopCoe <;> simp [mul_def] <;> rfl
60+
#align with_top.top_mul' WithTop.top_mul'
61+
62+
@[simp] theorem top_mul {a : WithTop α} (h : a ≠ 0) : ⊤ * a = ⊤ := by rw [top_mul', if_neg h]
5763
#align with_top.top_mul WithTop.top_mul
5864

65+
theorem mul_eq_top_iff {a b : WithTop α} : a * b = ⊤ ↔ a ≠ 0 ∧ b = ⊤ ∨ a = ⊤ ∧ b ≠ 0 := by
66+
rw [mul_def, ite_eq_iff, ← none_eq_top, Option.map₂_eq_none_iff]
67+
have ha : a = 0 → a ≠ none := fun h => h.symm ▸ zero_ne_top
68+
have hb : b = 0 → b ≠ none := fun h => h.symm ▸ zero_ne_top
69+
tauto
70+
#align with_top.mul_eq_top_iff WithTop.mul_eq_top_iff
71+
72+
theorem mul_lt_top' [LT α] {a b : WithTop α} (ha : a < ⊤) (hb : b < ⊤) : a * b < ⊤ := by
73+
rw [WithTop.lt_top_iff_ne_top] at *
74+
simp only [Ne.def, mul_eq_top_iff, *, and_false, false_and, false_or]
75+
#align with_top.mul_lt_top' WithTop.mul_lt_top'
76+
77+
theorem mul_lt_top [LT α] {a b : WithTop α} (ha : a ≠ ⊤) (hb : b ≠ ⊤) : a * b < ⊤ :=
78+
mul_lt_top' (WithTop.lt_top_iff_ne_top.2 ha) (WithTop.lt_top_iff_ne_top.2 hb)
79+
#align with_top.mul_lt_top WithTop.mul_lt_top
80+
5981
instance noZeroDivisors [NoZeroDivisors α] : NoZeroDivisors (WithTop α) := by
6082
refine ⟨fun h₁ => Decidable.by_contradiction <| fun h₂ => ?_⟩
6183
rw [mul_def, if_neg h₂] at h₁
@@ -68,7 +90,7 @@ section MulZeroClass
6890

6991
variable [MulZeroClass α]
7092

71-
@[norm_cast]
93+
@[simp, norm_cast]
7294
theorem coe_mul {a b : α} : (↑(a * b) : WithTop α) = a * b := by
7395
by_cases ha : a = 0
7496
· simp [ha]
@@ -87,23 +109,6 @@ theorem mul_coe {b : α} (hb : b ≠ 0) : ∀ {a : WithTop α},
87109
rfl
88110
#align with_top.mul_coe WithTop.mul_coe
89111

90-
@[simp]
91-
theorem mul_eq_top_iff {a b : WithTop α} : a * b = ⊤ ↔ a ≠ 0 ∧ b = ⊤ ∨ a = ⊤ ∧ b ≠ 0 := by
92-
match a with
93-
| none => match b with
94-
| none => simp [none_eq_top]
95-
| Option.some b => by_cases hb : b = 0 <;> simp [none_eq_top, some_eq_coe, hb]
96-
| Option.some a => match b with
97-
| none => by_cases ha : a = 0 <;> simp [none_eq_top, some_eq_coe, ha]
98-
| Option.some b => simp [some_eq_coe, ← coe_mul]
99-
#align with_top.mul_eq_top_iff WithTop.mul_eq_top_iff
100-
101-
theorem mul_lt_top [Preorder α] {a b : WithTop α} (ha : a ≠ ⊤) (hb : b ≠ ⊤) : a * b < ⊤ := by
102-
lift a to α using ha
103-
lift b to α using hb
104-
simp only [← coe_mul, coe_lt_top]
105-
#align with_top.mul_lt_top WithTop.mul_lt_top
106-
107112
@[simp]
108113
theorem untop'_zero_mul (a b : WithTop α) : (a * b).untop' 0 = a.untop' 0 * b.untop' 0 := by
109114
by_cases ha : a = 0; · rw [ha, zero_mul, ← coe_zero, untop'_coe, zero_mul]
@@ -148,7 +153,7 @@ protected def MonoidWithZeroHom.withTopMap {R S : Type _} [MulZeroOneClass R] [D
148153
induction' y using WithTop.recTopCoe with y
149154
· have : (f x : WithTop S) ≠ 0 := by simpa [hf.eq_iff' (map_zero f)] using hx
150155
simp [mul_top hx, mul_top this]
151-
· simp [← coe_mul, map_coe] }
156+
· simp only [map_coe, ← coe_mul, map_mul] } -- porting note: todo: `simp [← coe_mul]` fails
152157
#align monoid_with_zero_hom.with_top_map WithTop.MonoidWithZeroHom.withTopMap
153158

154159
instance [SemigroupWithZero α] [NoZeroDivisors α] : SemigroupWithZero (WithTop α) :=
@@ -250,13 +255,25 @@ theorem bot_mul_bot : (⊥ * ⊥ : WithBot α) = ⊥ :=
250255
WithTop.top_mul_top
251256
#align with_bot.bot_mul_bot WithBot.bot_mul_bot
252257

258+
theorem mul_eq_bot_iff {a b : WithBot α} : a * b = ⊥ ↔ a ≠ 0 ∧ b = ⊥ ∨ a = ⊥ ∧ b ≠ 0 :=
259+
WithTop.mul_eq_top_iff
260+
#align with_bot.mul_eq_bot_iff WithBot.mul_eq_bot_iff
261+
262+
theorem bot_lt_mul' [LT α] {a b : WithBot α} (ha : ⊥ < a) (hb : ⊥ < b) : ⊥ < a * b :=
263+
WithTop.mul_lt_top' (α := αᵒᵈ) ha hb
264+
#align with_bot.bot_lt_mul' WithBot.bot_lt_mul'
265+
266+
theorem bot_lt_mul [LT α] {a b : WithBot α} (ha : a ≠ ⊥) (hb : b ≠ ⊥) : ⊥ < a * b :=
267+
WithTop.mul_lt_top (α := αᵒᵈ) ha hb
268+
#align with_bot.bot_lt_mul WithBot.bot_lt_mul
269+
253270
end Mul
254271

255272
section MulZeroClass
256273

257274
variable [MulZeroClass α]
258275

259-
@[norm_cast]
276+
@[simp, norm_cast] -- porting note: added `simp`
260277
theorem coe_mul {a b : α} : (↑(a * b) : WithBot α) = a * b :=
261278
WithTop.coe_mul
262279
#align with_bot.coe_mul WithBot.coe_mul
@@ -266,17 +283,6 @@ theorem mul_coe {b : α} (hb : b ≠ 0) {a : WithBot α} :
266283
WithTop.mul_coe hb
267284
#align with_bot.mul_coe WithBot.mul_coe
268285

269-
@[simp]
270-
theorem mul_eq_bot_iff {a b : WithBot α} : a * b = ⊥ ↔ a ≠ 0 ∧ b = ⊥ ∨ a = ⊥ ∧ b ≠ 0 :=
271-
WithTop.mul_eq_top_iff
272-
#align with_bot.mul_eq_bot_iff WithBot.mul_eq_bot_iff
273-
274-
theorem bot_lt_mul [Preorder α] {a b : WithBot α} (ha : ⊥ < a) (hb : ⊥ < b) : ⊥ < a * b := by
275-
lift a to α using ne_bot_of_gt ha
276-
lift b to α using ne_bot_of_gt hb
277-
simp only [← coe_mul, bot_lt_coe]
278-
#align with_bot.bot_lt_mul WithBot.bot_lt_mul
279-
280286
end MulZeroClass
281287

282288
/-- `Nontrivial α` is needed here as otherwise we have `1 * ⊥ = ⊥` but also `= 0 * ⊥ = 0`. -/

‎Mathlib/Algebra/Order/Sub/WithTop.lean‎

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Floris van Doorn
55
66
! This file was ported from Lean 3 source module algebra.order.sub.with_top
7-
! leanprover-community/mathlib commit 10b4e499f43088dd3bb7b5796184ad5216648ab1
7+
! leanprover-community/mathlib commit afdb4fa3b32d41106a4a09b371ce549ad7958abd
88
! Please do not edit these lines, except to modify the commit id
99
! if you have ported upstream changes.
1010
-/
@@ -48,6 +48,12 @@ theorem top_sub_coe {a : α} : (⊤ : WithTop α) - a = ⊤ :=
4848
theorem sub_top {a : WithTop α} : a - ⊤ = 0 := by cases a <;> rfl
4949
#align with_top.sub_top WithTop.sub_top
5050

51+
@[simp] theorem sub_eq_top_iff {a b : WithTop α} : a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤ := by
52+
induction a using recTopCoe <;> induction b using recTopCoe <;>
53+
simp only [← coe_sub, coe_ne_top, sub_top, zero_ne_top, coe_ne_top, top_sub_coe, false_and,
54+
Ne.def]
55+
#align with_top.sub_eq_top_iff WithTop.sub_eq_top_iff
56+
5157
theorem map_sub [Sub β] [Zero β] {f : α → β} (h : ∀ x y, f (x - y) = f x - f y) (h₀ : f 0 = 0) :
5258
∀ x y : WithTop α, (x - y).map f = x.map f - y.map f
5359
| _, ⊤ => by simp only [h₀, sub_top, WithTop.map_zero, coe_zero, map_top]

0 commit comments

Comments
 (0)