Skip to content

Commit

Permalink
chore Set/UnionLift: generalize to Sort (#4071)
Browse files Browse the repository at this point in the history
Co-authored-by: Komyyy <pol_tta@outlook.jp>
  • Loading branch information
ChrisHughes24 and Komyyy committed May 19, 2023
1 parent bd2d76d commit 83998c1
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions Mathlib/Data/Set/UnionLift.lean
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

0 comments on commit 83998c1

Please sign in to comment.