# Zulip Chat Archive

## Stream: new members

### Topic: Metric space question

#### Jason KY. (Mar 26 2020 at 14:23):

Hi,

I have proved that the product of two metric spaces is also a metric space:

import topology.metric_space.basic noncomputable theory variables {X : Type*} [metric_space X] variables {Y : Type*} [metric_space Y] /- The metric of any two elements of a metric space is non-negative -/ theorem metric_nonneg : ∀ x y : X, 0 ≤ dist x y := λ x y, begin suffices : 0 ≤ dist y x + dist x y - dist y y, rw [dist_self, dist_comm, sub_zero] at this, linarith, linarith [dist_triangle y x y] end /- The product of two metric spaces is also a metric space -/ instance : metric_space (X × Y) := { dist := λ ⟨x₀, y₀⟩ ⟨x₁, y₁⟩, dist x₀ x₁ + dist y₀ y₁, dist_self := λ ⟨x, y⟩, show dist x x + dist y y = 0, by simp, eq_of_dist_eq_zero := -- Why can't I use λ ⟨x₀, y₀⟩ ⟨x₁, y₁⟩ here? begin rintros ⟨x₀, y₀⟩ ⟨x₁, y₁⟩, show dist x₀ x₁ + dist y₀ y₁ = 0 → (x₀, y₀) = (x₁, y₁), intro h, suffices : dist x₀ x₁ = 0 ∧ dist y₀ y₁ = 0, rwa [eq_of_dist_eq_zero this.left, eq_of_dist_eq_zero this.right], split, all_goals {linarith [metric_nonneg x₀ x₁, metric_nonneg y₀ y₁, h]} end, dist_comm := λ ⟨x₀, y₀⟩ ⟨x₁, y₁⟩, show dist x₀ x₁ + dist y₀ y₁ = dist x₁ x₀ + dist y₁ y₀, by simp [dist_comm], dist_triangle := λ ⟨x₀, y₀⟩ ⟨x₁, y₁⟩ ⟨x₂, y₂⟩, show dist x₀ x₂ + dist y₀ y₂ ≤ dist x₀ x₁ + dist y₀ y₁ + (dist x₁ x₂ + dist y₁ y₂), by linarith [dist_triangle x₀ x₁ x₂, dist_triangle y₀ y₁ y₂] }

but as you can see in my proof that the product of two metric spaces is also a metric space, I wasn't able to use `λ ⟨x₀, y₀⟩ ⟨x₁, y₁⟩`

when proving `eq_of_dist_eq_zero`

. Why might this be?

#### Reid Barton (Mar 26 2020 at 15:53):

What happens when you try?

#### Jason KY. (Mar 26 2020 at 16:19):

It gives me

__mlocal__fresh_2827_71439 : X × Y, _x : dist (x₀, y₀) __mlocal__fresh_2827_71439 = 0, _fun_match : dist (x₀, y₀) __mlocal__fresh_2827_71439 = 0 → (x₀, y₀) = __mlocal__fresh_2827_71439

when I want

x₀ : X, y₀ : Y, x₁ : X, y₁ : Y

which is what `rintro`

gives me

#### Reid Barton (Mar 26 2020 at 16:30):

Weird. I have no idea.

#### Jason KY. (Mar 27 2020 at 14:17):

I'm currently trying to define a category of metric spaces but I've gotten stuck when trying to define a mapping between two metric spaces.

import topology.metric_space.basic import category_theory.concrete_category open category_theory definition Metric_space := bundled metric_space variables {X Y : Metric_space} variables {f : X.1 → Y.1} -- invalid universe declaration, 'u_1' shadows a local universe

As you can see, I received the error `invalid universe declaration, 'u_1' shadows a local universe`

when trying to define a mapping. What does this mean and how can I fix this?

#### Reid Barton (Mar 27 2020 at 14:19):

I don't really know why this happens, but it's better to be explicit with universe levels (just like you would write `Type u`

)

#### Jason KY. (Mar 27 2020 at 14:20):

How would I be explicit with universe levels in this case? Sorry I don't normally use universes :/

#### Reid Barton (Mar 27 2020 at 14:24):

probably something like (untested)

import topology.metric_space.basic import category_theory.concrete_category universe u open category_theory definition Metric_space := bundled metric_space.{u} variables {X Y : Metric_space.{u}} variables {f : X.1 → Y.1}

#### Jason KY. (Mar 27 2020 at 14:24):

Ah! That works perfectly! Thanks

#### Jason KY. (Mar 28 2020 at 13:26):

Hi again!

I'm currently proving that the finite union of bounded sets is also bounded

/- The union of finitely many bounded subsets is also bounded -/ theorem bounded_union (S : ℕ → set X) (h₀ : ∀ n : ℕ, is_bounded $ S n) : ∀ n : ℕ, is_bounded $ ⋃ i ∈ finset.range n, S i | 0 := by simp; constructor; refl | (n + 1) := by simp [bounded_union_two, bounded_union]

And I'm receiving this error

failed to prove recursive application is decreasing, well founded relation @has_well_founded.r ℕ (@has_well_founded_of_has_sizeof ℕ nat.has_sizeof) Possible solutions: - Use 'using_well_founded' keyword in the end of your definition to specify tactics for synthesizing well founded relations and decreasing proofs. - The default decreasing tactic uses the 'assumption' tactic, thus hints (aka local proofs) can be provided using 'have'-expressions. The nested exception contains the failure state for the decreasing tactic. nested exception message: failed

I don't really understand what the possible solutions mean, any help would be appreciated!

#### Kenny Lau (Mar 28 2020 at 13:28):

if you include `bounded_union`

then I suspect it will just use `bounded_union`

on `n+1`

#### Jason KY. (Mar 28 2020 at 13:31):

Right, that's probably it

#### Jason KY. (Mar 28 2020 at 13:33):

Actually I'm not sure, I have`bounded_union : ∀ (n : ℕ), is_bounded (⋃ (i : ℕ) (H : i ∈ finset.range n), S i)`

as a hypothesis. Will `simp`

not use this instead?

#### Jason KY. (Mar 28 2020 at 13:34):

Is there a way to manually name this inductive hypothesis so it's less confusing?

#### Kenny Lau (Mar 28 2020 at 13:35):

it would be easier for me to help you if you would produce an MWE

#### Jason KY. (Mar 28 2020 at 13:36):

Alright, will do!

#### Jason KY. (Mar 28 2020 at 13:38):

This should work

import topology.metric_space.basic variables {X : Type*} [metric_space X] /- Notion of boundedness on metric spaces -/ def is_bounded (S : set X) := S = ∅ ∨ ∃ x₀ ∈ S, ∃ k : ℝ, ∀ x ∈ S, dist x x₀ ≤ k /- The union of two bounded subsets is also bounded -/ lemma bounded_union_two (S T : set X) (hs : is_bounded S) (ht : is_bounded T) : is_bounded $ S ∪ T := sorry /- The union of finitely many bounded subsets is also bounded -/ theorem bounded_union (S : ℕ → set X) (h₀ : ∀ n : ℕ, is_bounded $ S n) : ∀ n : ℕ, is_bounded $ ⋃ i ∈ finset.range n, S i | 0 := by simp; constructor; refl | (n + 1) := by simp [bounded_union_two, bounded_union]

#### Kenny Lau (Mar 28 2020 at 13:40):

I don't think `⋃ i ∈ finset.range n`

is idiomatic

#### Reid Barton (Mar 28 2020 at 13:41):

Since `n`

is an explicit argument, does it help if you just put `bounded_union n`

in simp?

#### Jason KY. (Mar 28 2020 at 13:41):

Kenny Lau said:

I don't think

`⋃ i ∈ finset.range n`

is idiomatic

Sorry but what does idiomatic mean?

#### Jason KY. (Mar 28 2020 at 13:43):

Reid Barton said:

Since

`n`

is an explicit argument, does it help if you just put`bounded_union n`

in simp?

Emm, then `simp`

doesn't solve the goal, but maybe it's working as intended then?

#### Kenny Lau (Mar 28 2020 at 13:43):

import topology.metric_space.basic variables {X : Type*} [metric_space X] /- Notion of boundedness on metric spaces -/ def is_bounded (S : set X) := S = ∅ ∨ ∃ x₀ ∈ S, ∃ k : ℝ, ∀ x ∈ S, dist x x₀ ≤ k /- The union of two bounded subsets is also bounded -/ lemma bounded_union_two (S T : set X) (hs : is_bounded S) (ht : is_bounded T) : is_bounded $ S ∪ T := sorry /- The union of finitely many bounded subsets is also bounded -/ theorem bounded_union (S : ℕ → set X) (h₀ : ∀ n : ℕ, is_bounded $ S n) : ∀ n : ℕ, is_bounded $ finset.sup (finset.range n) S | 0 := by left; simp; refl | (n + 1) := by simpa [finset.range_succ] using bounded_union_two _ _ (h₀ _) (bounded_union n)

#### Reid Barton (Mar 28 2020 at 13:43):

Jason KY. said:

Kenny Lau said:

I don't think

`⋃ i ∈ finset.range n`

is idiomaticSorry but what does idiomatic mean?

The normal way to write something. Consider `⋃ i < n`

.

#### Kenny Lau (Mar 28 2020 at 13:44):

Jason KY. said:

Kenny Lau said:

I don't think

`⋃ i ∈ finset.range n`

is idiomaticSorry but what does idiomatic mean?

idiomatic means the same in English as in here: how people would say it

#### Jason KY. (Mar 28 2020 at 13:44):

Ah, alright!

#### Kenny Lau (Mar 28 2020 at 13:44):

Reid Barton said:

Jason KY. said:

Kenny Lau said:

I don't think

`⋃ i ∈ finset.range n`

is idiomaticSorry but what does idiomatic mean?

The normal way to write something. Consider

`⋃ i < n`

.

I... don't think that's idiomatic either

#### Kenny Lau (Mar 28 2020 at 13:44):

because there's not enough lemmas to reduce from n+1 to n

#### Jason KY. (Mar 28 2020 at 13:46):

Right, I'll try to use `finset.sup`

in the future then, thanks for the help!

#### Kenny Lau (Mar 28 2020 at 13:47):

I don't know what's idiomatic actually. When do we use a finite union?

#### Kenny Lau (Mar 28 2020 at 13:47):

I mean, this lemma has nothing to do with `is_bounded`

: it's just induction from `bounded_union_two`

#### Reid Barton (Mar 28 2020 at 13:47):

ok yes

#### Reid Barton (Mar 28 2020 at 13:48):

lemma set.finite.compact_bUnion {s : set β} {f : β → set α} (hs : finite s) (hf : ∀i ∈ s, compact (f i)) : compact (⋃i ∈ s, f i) :=

#### Reid Barton (Mar 28 2020 at 13:48):

lemma compact_Union {f : β → set α} [fintype β] (h : ∀i, compact (f i)) : compact (⋃i, f i) :=

#### Kenny Lau (Mar 28 2020 at 13:48):

huh

#### Reid Barton (Mar 28 2020 at 13:48):

I didn't really pay attention to the whole statement of Jason's lemma.

#### Jason KY. (Mar 28 2020 at 13:49):

Emm, I'm a bit confused. When should we use what?

#### Jason KY. (Mar 28 2020 at 13:54):

I was able to get it working by introducing a temp lemma

lemma temp (S : ℕ → set X) (n : ℕ) : (⋃ i ∈ finset.range (n + 1), S i) = (⋃ i ∈ finset.range n, S i) ∪ S (n + 1) := sorry /- The union of finitely many bounded subsets is also bounded -/ theorem bounded_union (S : ℕ → set X) (h₀ : ∀ n : ℕ, is_bounded $ S n) : ∀ n : ℕ, is_bounded $ ⋃ i ∈ finset.range n, S i | 0 := by simp; constructor; refl | (n + 1) := by simp [temp, bounded_union_two, bounded_union n, h₀ (n + 1)]

Is there something like `temp`

in mathlib?

#### Reid Barton (Mar 28 2020 at 13:55):

I would suggest imitating the statement of `set.finite.compact_bUnion`

and using `finset.induction_on`

in the proof

#### Reid Barton (Mar 28 2020 at 13:56):

Your statement is not going to be very convenient to use anyways so why bother proving it?

#### Reid Barton (Mar 28 2020 at 13:56):

Unless it happens to be exactly what you need for some application

#### Jason KY. (Mar 28 2020 at 13:57):

Oh, I'm just learning metric spaces myself so I thought to prove all the theorems in my lecture notes in LEAN

#### Jason KY. (Mar 28 2020 at 13:57):

Reid Barton said:

I would suggest imitating the statement of

`set.finite.compact_bUnion`

and using`finset.induction_on`

in the proof

Right, I'll try to do this

#### Reid Barton (Mar 28 2020 at 13:58):

Normally the finite set indexing your sets won't happen to be of the form `finset.range n`

and then you would have to do a lot of work to massage things into a situation in which you can apply your `bounded_union`

.

#### Jason KY. (Mar 29 2020 at 16:29):

Hi,

I would now like to define the notion of open in LEAN however I've gotten a bit stuck.

/- Definition of an open ball -/ def open_ball (x₀ : X) (r : ℝ) (h : 0 < r) := {x : X | dist x₀ x < r} /- Definition of being open -/ def is_open' (S : set X) := ∀ s ∈ S, ∃ ε > 0, open_ball s ε H ⊆ S

As you can see, my definition of an open ball requires the radius to be positive but this makes things rather awkward as then I would need to refer to a proof that `r > 0`

whenever I would like to create an open ball.

/- Definition of being open -/ def is_open' (S : set X) := ∀ s ∈ S, ∃ ε : ℝ, (hε : 0 < ε), open_ball s ε hε ⊆ S

I was hoping something like this would work but unfortunately, it does not. Is there an easy way of doing this? (Or even better, perhaps a type called`ℝ⁺`

which is the positive reals?)

#### Patrick Massot (Mar 29 2020 at 16:31):

I think you have too many commas.

#### Patrick Massot (Mar 29 2020 at 16:32):

But I can't be sure because you didn't provide a MWE.

#### Reid Barton (Mar 29 2020 at 16:32):

`∀ s ∈ S, ∃ (ε : ℝ) (hε : 0 < ε), open_ball s ε hε ⊆ S`

#### Reid Barton (Mar 29 2020 at 16:32):

is at least syntactically correct

#### Jason KY. (Mar 29 2020 at 16:33):

Ah, I see! thanks!

#### Patrick Massot (Mar 29 2020 at 16:34):

But it's still a bad idea to include the positivity constraint in the definition of open_ball.

#### Jason KY. (Mar 29 2020 at 16:35):

is it? It's what my lecture notes said atleast

#### Patrick Massot (Mar 29 2020 at 16:36):

Your lecture notes don't include type theoretic convenience constraints.

#### Jason KY. (Mar 29 2020 at 16:37):

Why would it be a bad idea with these constraints?

#### Patrick Massot (Mar 29 2020 at 16:40):

You saw why putting this in the definition of balls is a bad idea.

#### Jason KY. (Mar 29 2020 at 16:43):

Right... But I don't see a better solution if I would like to use the definition presented in my lecture notes so I guess I just have to deal with it :D

#### Patrick Massot (Mar 29 2020 at 16:45):

I think your lecturer wouldn't notice this difference in the definition of balls. Of course the definition of open subsets must include a positive radius condition.

#### Jason KY. (Mar 29 2020 at 16:47):

Okay, I'll try to do without this restriction and just apply the positive radius and see if I run into trouble. Thanks again!

#### Patrick Massot (Mar 29 2020 at 16:48):

I mean you can change your code to

/- Definition of an open ball -/ def open_ball (x₀ : X) (r : ℝ) := {x : X | dist x₀ x < r} /- Definition of being open -/ def is_open' (S : set X) := ∀ s ∈ S, ∃ ε > 0, open_ball s ε ⊆ S

#### Jason KY. (Mar 29 2020 at 16:49):

I've changed it to this because I've heard you should always use `<`

rather than `>`

/- Definition of being open -/ def is_open' (S : set X) := ∀ s ∈ S, ∃ (ε : ℝ) (hε : 0 < ε), open_ball s ε ⊆ S

#### Jason KY. (Mar 29 2020 at 16:50):

But I guess it doesn't really matter either way

#### Patrick Massot (Mar 29 2020 at 16:50):

I would keep the natural writing order here.

#### Kevin Buzzard (Mar 29 2020 at 17:17):

Oh! There are cases when `>`

is OK?

#### Patrick Massot (Mar 29 2020 at 17:18):

I'm lobbying that it should be allowed precisely in this case (when appearing in a quantifier).

#### Kevin Buzzard (Mar 29 2020 at 17:27):

That's interesting because appearing in a quantifier of this form is the only time I ever miss `>`

but I tell Xenaites to use `<`

or else they'll get linted.

#### Patrick Massot (Mar 29 2020 at 17:28):

You can always plea the linter's indulgence.

#### Patrick Massot (Mar 29 2020 at 17:29):

with `@[nolint ge_or_gt]`

#### Jason KY. (Mar 31 2020 at 18:20):

Following @Reid Barton 's suggestion, I've been trying to use `set.finite.induction_on`

but I'm not sure if the way I'm using it is correct.

Below is a MWE of my current problem:

import topology.metric_space.basic variables {X : Type*} [metric_space X] /- Definition of an open ball -/ def open_ball (x₀ : X) (r : ℝ) := {x : X | dist x₀ x < r} /- Definition of being open -/ def is_open' (S : set X) := ∀ s ∈ S, ∃ (ε : ℝ) (hε : 0 < ε), open_ball s ε ⊆ S /- The intersect of open sets is open -/ lemma inter_open_is_open (U₀ U₁ : set X) (h₀ : is_open' U₀) (h₁ : is_open' U₁) : is_open' (U₀ ∩ U₁) := sorry lemma inter_finite_open_is_open (I : set ℕ) (U : ℕ → set X) {hI : set.finite I} (h₀ : ∀ i ∈ I, is_open' $ U i) : is_open' $ ⋂ i ∈ I, U i := set.finite.induction_on hI (λ x, by simp; from ⟨1, by norm_num⟩) $ λ i S hi hS hopen, begin rw set.bInter_insert, apply inter_open_is_open, {apply h₀, sorry}, assumption end

I feel that after applying induction, there should be a term like `is_open' (U i)`

but there is not. What have I done wrong here?

#### Alex J. Best (Mar 31 2020 at 18:33):

If you move `h₀`

into the statement you can make it work, caveat lector: I didn't think too hard about the best way to do it, just followed my nose at every subgoal.

lemma inter_finite_open_is_open (I : set ℕ) (U : ℕ → set X) {hI : set.finite I} : ( ∀ i ∈ I, is_open' $ U i) → (is_open' $ ⋂ i ∈ I, U i) := set.finite.induction_on hI (λ x, by simp; begin intro, intro, use 1, split, exact zero_lt_one,exact set.subset_univ (open_ball s 1), end) $ λ i S hi hS hopen, begin rw set.bInter_insert,intros, apply inter_open_is_open, {apply a, exact set.mem_insert i S, }, apply hopen,intros, apply a,exact set.mem_union_right (λ (a : ℕ), a = i) H, end

#### Jason KY. (Mar 31 2020 at 18:35):

Thank you so much Alex!

#### Jason KY. (Mar 31 2020 at 18:37):

I'll try to put such predicates in the statement in the future. Don't think it would hurt right?

#### Alex J. Best (Mar 31 2020 at 18:42):

Well normally its annoying to have to explicitly intro them and name them at the start of the proof, but for induction type proofs, its sometimes needed.

#### Jason KY. (Apr 04 2020 at 17:31):

Hi!

I'm slightly stuck on trying to manipulate the following intersect

import topology.metric_space.basic variables {X : Type*} [metric_space X] /- Definition of an open ball -/ def open_ball (x₀ : X) (r : ℝ) := {x : X | dist x₀ x < r} /- Definition of being open -/ def is_open' (S : set X) := ∀ s ∈ S, ∃ (ε : ℝ) (hε : 0 < ε), open_ball s ε ⊆ S /- Definition of being closed -/ def is_closed' (S : set X) := is_open' $ -S /- Definition of closure -/ def closure' (S : set X) := ⋂ (T : set X) (h₀ : S ⊆ T) (h₁ : is_closed' T), T attribute [reducible] open_ball is_open' is_closed' lemma closure_closed (S : set X) : is_closed' $ closure' S := begin unfold closure', -- ⊢ is_closed' (⋂ (T : set X) (h₀ : S ⊆ T) (h₁ : is_closed' T), T) sorry end

I would like to use a lemma I've proved which it that the intersect of closed sets is closed :

theorem Inter_closed_is_closed (I : set Type*) (U : Type* → set X) (h : ∀ i ∈ I, is_closed' $ U i) : is_closed' $ ⋂ i ∈ I, U i := sorry

How should I go about doing this?

#### Reid Barton (Apr 04 2020 at 17:36):

The statement of your lemma is not good. Compare `is_open_bUnion`

.

#### Jason KY. (Apr 04 2020 at 17:40):

Is the statement bad because of the squiggly brackets or because of the `Type*`

s?

#### Reid Barton (Apr 04 2020 at 17:41):

The `Type*`

s

#### Reid Barton (Apr 04 2020 at 17:41):

You should replace those with an arbitrary type

#### Jason KY. (Apr 04 2020 at 17:42):

Like this?

theorem Inter_closed_is_closed (I : set Type) (U : Type → set X) (h : ∀ i ∈ I, is_closed' $ U i) : is_closed' $ ⋂ i ∈ I, U i := sorry

#### Reid Barton (Apr 04 2020 at 17:54):

No, what is `set Type`

for? I think you are confusing `Type`

with the concept of "some type". Study what happens near the start of `topology.basic`

.

#### Jason KY. (Apr 04 2020 at 17:56):

Ah, I see. So it should be like this?

variable {α : Type*} theorem Inter_closed_is_closed {I : set α} {U : α → set X} (h : ∀ i ∈ I, is_closed' $ U i) : is_closed' $ ⋂ i ∈ I, U i := sorry

#### Reid Barton (Apr 04 2020 at 17:57):

Yes. you might find you need additional lemmas though, I'm not sure.

#### Jason KY. (Apr 04 2020 at 17:58):

I think it works, let me try to finish the proof

#### Jason KY. (Apr 04 2020 at 18:11):

I couldn't get it working :/ But if I change the definition of my closure then it works:

/- Definition of closure -/ def closure'' (S : set X) := ⋂ (T : set X) (h₀ : S ⊆ T ∧ is_closed' T), T /- The closure of a set is also closed -/ lemma closure_closed (S : set X) : is_closed' $ closure'' S := Inter_closed_is_closed $ begin intros T hT, from hT.right end

It there a way to change `⋂ (T : set X) (h₀ : S ⊆ T) (h₁ : is_closed' T), T`

to ` ⋂ (T : set X) (h₀ : S ⊆ T ∧ is_closed' T), T`

.

They are the same right?

#### Mario Carneiro (Apr 04 2020 at 18:12):

did you try simp?

#### Mario Carneiro (Apr 04 2020 at 18:12):

that's the sort of thing that `simp`

is likely to know

#### Jason KY. (Apr 04 2020 at 18:13):

Just tried it, doesn't work :/

#### Mario Carneiro (Apr 04 2020 at 18:13):

The lemma you need is `infi_and`

, not sure if that has a set version but it's defeq to it

#### Jason KY. (Apr 04 2020 at 18:15):

Alright, I'll try it out!

#### Mario Carneiro (Apr 04 2020 at 18:19):

You should prove the version without the set, because it is more general

theorem Inter_closed_is_closed {α} {U : α → set X} (h : ∀ i, is_closed' $ U i) : is_closed' $ ⋂ i, U i := sorry variable {α : Type*} theorem bInter_closed_is_closed {I : set α} {U : α → set X} (h : ∀ i ∈ I, is_closed' $ U i) : is_closed' $ ⋂ i ∈ I, U i := Inter_closed_is_closed $ λ i, Inter_closed_is_closed $ λ h', h i h'

#### Mario Carneiro (Apr 04 2020 at 18:20):

def closure' (S : set X) := ⋂ (T : set X) (h₀ : S ⊆ T) (h₁ : is_closed' T), T /- The closure of a set is also closed -/ lemma closure_closed (S : set X) : is_closed' $ closure' S := Inter_closed_is_closed $ λ T, Inter_closed_is_closed $ λ h₁, Inter_closed_is_closed $ λ h₂, h₂

#### Mario Carneiro (Apr 04 2020 at 18:22):

Note that `Inter_closed_is_closed`

has its own version of `{α}`

, which is actually `{α : Sort*}`

, so that it can also apply when the index type is a prop

#### Mario Carneiro (Apr 04 2020 at 18:22):

if you reuse the variable it will be `{α : Type*}`

which doesn't apply to Prop

#### Jason KY. (Apr 04 2020 at 18:25):

So `{α}`

is just short for `{α : Sort*}`

?

#### Mario Carneiro (Apr 04 2020 at 18:27):

Yes. Note that `Sort*`

is actually `Sort _`

, a metavariable that will be instantiated depending on the rest of the statement. So for example if you use this in the second statement:

theorem bInter_closed_is_closed {α} {I : set α} {U : α → set X} (h : ∀ i ∈ I, is_closed' $ U i) : is_closed' $ ⋂ i ∈ I, U i := ...

then `{α}`

will get type `{α : Type u_1}`

because that's what is needed to make `set α`

typecheck

#### Jason KY. (Apr 04 2020 at 18:30):

Ah, I see. Thank you!

Last updated: May 14 2021 at 02:15 UTC