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] - chore Set/UnionLift: generalize to Sort #4071

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - chore Set/UnionLift: generalize to Sort #4071

Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
af0848a
chore Set/UnionLift: generalize to Sort
ChrisHughes24 May 18, 2023
1ca1917
preserve argument order
ChrisHughes24 May 18, 2023
d21e25d
match mathlib3 style. Set is Type _ -> Type _ so α is Type _ anyway
ChrisHughes24 May 18, 2023
2d4324f
update sha
Komyyy May 19, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions Mathlib/Data/Set/UnionLift.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Chris Hughes

! This file was ported from Lean 3 source module data.set.Union_lift
! leanprover-community/mathlib commit 207cfac9fcd06138865b5d04f7091e46d9320432
! leanprover-community/mathlib commit 5a4ea8453f128345f73cc656e80a49de2a54f481
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
Expand Down Expand Up @@ -41,7 +41,7 @@ constants, unary functions, or binary functions are preserved. These lemmas are:
directed union, directed supremum, glue, gluing
-/

variable {α ι β : Type _}
variable {α : Type _} {ι β : Sort _}

namespace Set

Expand Down