Skip to content

Commit

Permalink
bump to nightly-2023-05-06-16
Browse files Browse the repository at this point in the history 
mathlib commit leanprover-community/mathlib@3905fa8
  • Loading branch information
@leanprover-community-bot
leanprover-community-bot committed May 6, 2023
1 parent 2f9b6e1 commit 085548f
Show file tree
Hide file tree
Showing 3 changed files with 9 additions and 9 deletions.
6 changes: 3 additions & 3 deletions Mathbin/Topology/MetricSpace/Basic.lean
View file
Expand Up @@ -1614,7 +1614,7 @@ theorem totallyBounded_of_finite_discretization {s : Set α}
lean 3 declaration is
forall {α : Type.{u1}} [_inst_1 : PseudoMetricSpace.{u1} α] {s : Set.{u1} α}, (TotallyBounded.{u1} α (PseudoMetricSpace.toUniformSpace.{u1} α _inst_1) s) -> (forall (ε : Real), (GT.gt.{0} Real Real.hasLt ε (OfNat.ofNat.{0} Real 0 (OfNat.mk.{0} Real 0 (Zero.zero.{0} Real Real.hasZero)))) -> (Exists.{succ u1} (Set.{u1} α) (fun (t : Set.{u1} α) => Exists.{0} (HasSubset.Subset.{u1} (Set.{u1} α) (Set.hasSubset.{u1} α) t s) (fun (H : HasSubset.Subset.{u1} (Set.{u1} α) (Set.hasSubset.{u1} α) t s) => And (Set.Finite.{u1} α t) (HasSubset.Subset.{u1} (Set.{u1} α) (Set.hasSubset.{u1} α) s (Set.unionᵢ.{u1, succ u1} α α (fun (y : α) => Set.unionᵢ.{u1, 0} α (Membership.Mem.{u1, u1} α (Set.{u1} α) (Set.hasMem.{u1} α) y t) (fun (H : Membership.Mem.{u1, u1} α (Set.{u1} α) (Set.hasMem.{u1} α) y t) => Metric.ball.{u1} α _inst_1 y ε))))))))
but is expected to have type
forall {α : Type.{u1}} [_inst_1 : PseudoMetricSpace.{u1} α] {s : Set.{u1} α}, (TotallyBounded.{u1} α (PseudoMetricSpace.toUniformSpace.{u1} α _inst_1) s) -> (forall (ε : Real), (GT.gt.{0} Real Real.instLTReal ε (OfNat.ofNat.{0} Real 0 (Zero.toOfNat0.{0} Real Real.instZeroReal))) -> (Exists.{succ u1} (Set.{u1} α) (fun (t : Set.{u1} α) => And (HasSubset.Subset.{u1} (Set.{u1} α) (Set.instHasSubsetSet.{u1} α) t s) (And (Set.Finite.{u1} α t) (HasSubset.Subset.{u1} (Set.{u1} α) (Set.instHasSubsetSet.{u1} α) s (Set.unionᵢ.{u1, succ u1} α α (fun (y : α) => Set.unionᵢ.{u1, 0} α (Membership.mem.{u1, u1} α (Set.{u1} α) (Set.instMembershipSet.{u1} α) y t) (fun (h._@.Mathlib.Topology.MetricSpace.Basic._hyg.10746 : Membership.mem.{u1, u1} α (Set.{u1} α) (Set.instMembershipSet.{u1} α) y t) => Metric.ball.{u1} α _inst_1 y ε))))))))
forall {α : Type.{u1}} [_inst_1 : PseudoMetricSpace.{u1} α] {s : Set.{u1} α}, (TotallyBounded.{u1} α (PseudoMetricSpace.toUniformSpace.{u1} α _inst_1) s) -> (forall (ε : Real), (GT.gt.{0} Real Real.instLTReal ε (OfNat.ofNat.{0} Real 0 (Zero.toOfNat0.{0} Real Real.instZeroReal))) -> (Exists.{succ u1} (Set.{u1} α) (fun (t : Set.{u1} α) => And (HasSubset.Subset.{u1} (Set.{u1} α) (Set.instHasSubsetSet.{u1} α) t s) (And (Set.Finite.{u1} α t) (HasSubset.Subset.{u1} (Set.{u1} α) (Set.instHasSubsetSet.{u1} α) s (Set.unionᵢ.{u1, succ u1} α α (fun (y : α) => Set.unionᵢ.{u1, 0} α (Membership.mem.{u1, u1} α (Set.{u1} α) (Set.instMembershipSet.{u1} α) y t) (fun (h._@.Mathlib.Topology.MetricSpace.Basic._hyg.10766 : Membership.mem.{u1, u1} α (Set.{u1} α) (Set.instMembershipSet.{u1} α) y t) => Metric.ball.{u1} α _inst_1 y ε))))))))
Case conversion may be inaccurate. Consider using '#align metric.finite_approx_of_totally_bounded Metric.finite_approx_of_totallyBoundedₓ'. -/
/- ./././Mathport/Syntax/Translate/Basic.lean:635:2: warning: expanding binder collection (t «expr ⊆ » s) -/
theorem finite_approx_of_totallyBounded {s : Set α} (hs : TotallyBounded s) :
Expand Down Expand Up @@ -3816,7 +3816,7 @@ section Compact
lean 3 declaration is
forall {α : Type.{u1}} [_inst_2 : PseudoMetricSpace.{u1} α] {s : Set.{u1} α}, (IsCompact.{u1} α (UniformSpace.toTopologicalSpace.{u1} α (PseudoMetricSpace.toUniformSpace.{u1} α _inst_2)) s) -> (forall {e : Real}, (LT.lt.{0} Real Real.hasLt (OfNat.ofNat.{0} Real 0 (OfNat.mk.{0} Real 0 (Zero.zero.{0} Real Real.hasZero))) e) -> (Exists.{succ u1} (Set.{u1} α) (fun (t : Set.{u1} α) => Exists.{0} (HasSubset.Subset.{u1} (Set.{u1} α) (Set.hasSubset.{u1} α) t s) (fun (H : HasSubset.Subset.{u1} (Set.{u1} α) (Set.hasSubset.{u1} α) t s) => And (Set.Finite.{u1} α t) (HasSubset.Subset.{u1} (Set.{u1} α) (Set.hasSubset.{u1} α) s (Set.unionᵢ.{u1, succ u1} α α (fun (x : α) => Set.unionᵢ.{u1, 0} α (Membership.Mem.{u1, u1} α (Set.{u1} α) (Set.hasMem.{u1} α) x t) (fun (H : Membership.Mem.{u1, u1} α (Set.{u1} α) (Set.hasMem.{u1} α) x t) => Metric.ball.{u1} α _inst_2 x e))))))))
but is expected to have type
forall {α : Type.{u1}} [_inst_2 : PseudoMetricSpace.{u1} α] {s : Set.{u1} α}, (IsCompact.{u1} α (UniformSpace.toTopologicalSpace.{u1} α (PseudoMetricSpace.toUniformSpace.{u1} α _inst_2)) s) -> (forall {e : Real}, (LT.lt.{0} Real Real.instLTReal (OfNat.ofNat.{0} Real 0 (Zero.toOfNat0.{0} Real Real.instZeroReal)) e) -> (Exists.{succ u1} (Set.{u1} α) (fun (t : Set.{u1} α) => And (HasSubset.Subset.{u1} (Set.{u1} α) (Set.instHasSubsetSet.{u1} α) t s) (And (Set.Finite.{u1} α t) (HasSubset.Subset.{u1} (Set.{u1} α) (Set.instHasSubsetSet.{u1} α) s (Set.unionᵢ.{u1, succ u1} α α (fun (x : α) => Set.unionᵢ.{u1, 0} α (Membership.mem.{u1, u1} α (Set.{u1} α) (Set.instMembershipSet.{u1} α) x t) (fun (h._@.Mathlib.Topology.MetricSpace.Basic._hyg.25496 : Membership.mem.{u1, u1} α (Set.{u1} α) (Set.instMembershipSet.{u1} α) x t) => Metric.ball.{u1} α _inst_2 x e))))))))
forall {α : Type.{u1}} [_inst_2 : PseudoMetricSpace.{u1} α] {s : Set.{u1} α}, (IsCompact.{u1} α (UniformSpace.toTopologicalSpace.{u1} α (PseudoMetricSpace.toUniformSpace.{u1} α _inst_2)) s) -> (forall {e : Real}, (LT.lt.{0} Real Real.instLTReal (OfNat.ofNat.{0} Real 0 (Zero.toOfNat0.{0} Real Real.instZeroReal)) e) -> (Exists.{succ u1} (Set.{u1} α) (fun (t : Set.{u1} α) => And (HasSubset.Subset.{u1} (Set.{u1} α) (Set.instHasSubsetSet.{u1} α) t s) (And (Set.Finite.{u1} α t) (HasSubset.Subset.{u1} (Set.{u1} α) (Set.instHasSubsetSet.{u1} α) s (Set.unionᵢ.{u1, succ u1} α α (fun (x : α) => Set.unionᵢ.{u1, 0} α (Membership.mem.{u1, u1} α (Set.{u1} α) (Set.instMembershipSet.{u1} α) x t) (fun (h._@.Mathlib.Topology.MetricSpace.Basic._hyg.25516 : Membership.mem.{u1, u1} α (Set.{u1} α) (Set.instMembershipSet.{u1} α) x t) => Metric.ball.{u1} α _inst_2 x e))))))))
Case conversion may be inaccurate. Consider using '#align finite_cover_balls_of_compact finite_cover_balls_of_compactₓ'. -/
/- ./././Mathport/Syntax/Translate/Basic.lean:635:2: warning: expanding binder collection (t «expr ⊆ » s) -/
/-- Any compact set in a pseudometric space can be covered by finitely many balls of a given
Expand All @@ -3836,7 +3836,7 @@ theorem finite_cover_balls_of_compact {α : Type u} [PseudoMetricSpace α] {s :
lean 3 declaration is
forall {α : Type.{u1}} [_inst_2 : PseudoMetricSpace.{u1} α] {s : Set.{u1} α}, (IsCompact.{u1} α (UniformSpace.toTopologicalSpace.{u1} α (PseudoMetricSpace.toUniformSpace.{u1} α _inst_2)) s) -> (forall {e : Real}, (LT.lt.{0} Real Real.hasLt (OfNat.ofNat.{0} Real 0 (OfNat.mk.{0} Real 0 (Zero.zero.{0} Real Real.hasZero))) e) -> (Exists.{succ u1} (Set.{u1} α) (fun (t : Set.{u1} α) => Exists.{0} (HasSubset.Subset.{u1} (Set.{u1} α) (Set.hasSubset.{u1} α) t s) (fun (H : HasSubset.Subset.{u1} (Set.{u1} α) (Set.hasSubset.{u1} α) t s) => And (Set.Finite.{u1} α t) (HasSubset.Subset.{u1} (Set.{u1} α) (Set.hasSubset.{u1} α) s (Set.unionᵢ.{u1, succ u1} α α (fun (x : α) => Set.unionᵢ.{u1, 0} α (Membership.Mem.{u1, u1} α (Set.{u1} α) (Set.hasMem.{u1} α) x t) (fun (H : Membership.Mem.{u1, u1} α (Set.{u1} α) (Set.hasMem.{u1} α) x t) => Metric.ball.{u1} α _inst_2 x e))))))))
but is expected to have type
forall {α : Type.{u1}} [_inst_2 : PseudoMetricSpace.{u1} α] {s : Set.{u1} α}, (IsCompact.{u1} α (UniformSpace.toTopologicalSpace.{u1} α (PseudoMetricSpace.toUniformSpace.{u1} α _inst_2)) s) -> (forall {e : Real}, (LT.lt.{0} Real Real.instLTReal (OfNat.ofNat.{0} Real 0 (Zero.toOfNat0.{0} Real Real.instZeroReal)) e) -> (Exists.{succ u1} (Set.{u1} α) (fun (t : Set.{u1} α) => And (HasSubset.Subset.{u1} (Set.{u1} α) (Set.instHasSubsetSet.{u1} α) t s) (And (Set.Finite.{u1} α t) (HasSubset.Subset.{u1} (Set.{u1} α) (Set.instHasSubsetSet.{u1} α) s (Set.unionᵢ.{u1, succ u1} α α (fun (x : α) => Set.unionᵢ.{u1, 0} α (Membership.mem.{u1, u1} α (Set.{u1} α) (Set.instMembershipSet.{u1} α) x t) (fun (h._@.Mathlib.Topology.MetricSpace.Basic._hyg.25496 : Membership.mem.{u1, u1} α (Set.{u1} α) (Set.instMembershipSet.{u1} α) x t) => Metric.ball.{u1} α _inst_2 x e))))))))
forall {α : Type.{u1}} [_inst_2 : PseudoMetricSpace.{u1} α] {s : Set.{u1} α}, (IsCompact.{u1} α (UniformSpace.toTopologicalSpace.{u1} α (PseudoMetricSpace.toUniformSpace.{u1} α _inst_2)) s) -> (forall {e : Real}, (LT.lt.{0} Real Real.instLTReal (OfNat.ofNat.{0} Real 0 (Zero.toOfNat0.{0} Real Real.instZeroReal)) e) -> (Exists.{succ u1} (Set.{u1} α) (fun (t : Set.{u1} α) => And (HasSubset.Subset.{u1} (Set.{u1} α) (Set.instHasSubsetSet.{u1} α) t s) (And (Set.Finite.{u1} α t) (HasSubset.Subset.{u1} (Set.{u1} α) (Set.instHasSubsetSet.{u1} α) s (Set.unionᵢ.{u1, succ u1} α α (fun (x : α) => Set.unionᵢ.{u1, 0} α (Membership.mem.{u1, u1} α (Set.{u1} α) (Set.instMembershipSet.{u1} α) x t) (fun (h._@.Mathlib.Topology.MetricSpace.Basic._hyg.25516 : Membership.mem.{u1, u1} α (Set.{u1} α) (Set.instMembershipSet.{u1} α) x t) => Metric.ball.{u1} α _inst_2 x e))))))))
Case conversion may be inaccurate. Consider using '#align is_compact.finite_cover_balls IsCompact.finite_cover_ballsₓ'. -/
alias finite_cover_balls_of_compact ← IsCompact.finite_cover_balls
#align is_compact.finite_cover_balls IsCompact.finite_cover_balls
Expand Down
8 changes: 4 additions & 4 deletions lake-manifest.json
View file
Expand Up @@ -4,15 +4,15 @@
[{"git":
{"url": "https://github.com/leanprover-community/lean3port.git",
"subDir?": null,
"rev": "62041b9f44751a25347308a7237f0238f48b7ccd",
"rev": "99cc5c519c42090a977f2bb7911fec7819a57a6b",
"name": "lean3port",
"inputRev?": "62041b9f44751a25347308a7237f0238f48b7ccd"}},
"inputRev?": "99cc5c519c42090a977f2bb7911fec7819a57a6b"}},
{"git":
{"url": "https://github.com/leanprover-community/mathlib4.git",
"subDir?": null,
"rev": "b1a047acd503a2b450f242ef67c6f1c4da9ac020",
"rev": "38dbcd8285bc4b1391619c12f158a7409f3dfc12",
"name": "mathlib",
"inputRev?": "b1a047acd503a2b450f242ef67c6f1c4da9ac020"}},
"inputRev?": "38dbcd8285bc4b1391619c12f158a7409f3dfc12"}},
{"git":
{"url": "https://github.com/gebner/quote4",
"subDir?": null,
Expand Down
4 changes: 2 additions & 2 deletions lakefile.lean
View file
Expand Up @@ -4,7 +4,7 @@ open Lake DSL System
-- Usually the `tag` will be of the form `nightly-2021-11-22`.
-- If you would like to use an artifact from a PR build,
-- it will be of the form `pr-branchname-sha`.
def tag : String := "nightly-2023-05-06-14"
def tag : String := "nightly-2023-05-06-16"
def releaseRepo : String := "leanprover-community/mathport"
def oleanTarName : String := "mathlib3-binport.tar.gz"

Expand Down Expand Up @@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
untarReleaseArtifact releaseRepo tag oleanTarName libDir
return .nil

require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"62041b9f44751a25347308a7237f0238f48b7ccd"
require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"99cc5c519c42090a977f2bb7911fec7819a57a6b"

@[default_target]
lean_lib Mathbin where
Expand Down

0 comments on commit 085548f

Please sign in to comment.