Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat: port Analysis.BoxIntegral.Partition.Tagged #3669

Closed
wants to merge 13 commits into from
Closed

[Merged by Bors] - feat: port Analysis.BoxIntegral.Partition.Tagged #3669

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
21468c0
feat: port Analysis.BoxIntegral.Partition.Tagged
int-y1 Apr 27, 2023
90fd3f5
Initial file copy from mathport
int-y1 Apr 27, 2023
3463f3a
automated fixes
int-y1 Apr 27, 2023
e17f86b
fix names
int-y1 Apr 27, 2023
f76cc82
fix `forall_bunionᵢTagged` `unionᵢ_disjUnion`
int-y1 Apr 27, 2023
d5640f2
fix `tag_bunionᵢTagged`
int-y1 Apr 27, 2023
53b4252
docs
int-y1 Apr 27, 2023
bb43a1b
code style
int-y1 Apr 27, 2023
3241875
lint
int-y1 Apr 27, 2023
533aba4
Merge branch 'master' into port/Analysis.BoxIntegral.Partition.Tagged
int-y1 May 16, 2023
a753106
`unionᵢ` -> `iUnion`
int-y1 May 16, 2023
6baf112
fix `simps`
int-y1 May 16, 2023
80b5820
remove simp on `isHenstock_single`
int-y1 May 16, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
1 change: 1 addition & 0 deletions Mathlib.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -353,6 +353,7 @@ import Mathlib.Analysis.BoxIntegral.Box.Basic
import Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
import Mathlib.Analysis.BoxIntegral.Partition.Basic
import Mathlib.Analysis.BoxIntegral.Partition.Split
import Mathlib.Analysis.BoxIntegral.Partition.Tagged
import Mathlib.Analysis.Calculus.TangentCone
import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.Convex.Basic
Expand Down