Zulip Chat Archive

Stream: new members

Topic: Metric space question


view this post on Zulip 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?

view this post on Zulip Reid Barton (Mar 26 2020 at 15:53):

What happens when you try?

view this post on Zulip 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

view this post on Zulip Reid Barton (Mar 26 2020 at 16:30):

Weird. I have no idea.

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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 :/

view this post on Zulip 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}

view this post on Zulip Jason KY. (Mar 27 2020 at 14:24):

Ah! That works perfectly! Thanks

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Jason KY. (Mar 28 2020 at 13:31):

Right, that's probably it

view this post on Zulip Jason KY. (Mar 28 2020 at 13:33):

Actually I'm not sure, I havebounded_union : ∀ (n : ℕ), is_bounded (⋃ (i : ℕ) (H : i ∈ finset.range n), S i) as a hypothesis. Will simp not use this instead?

view this post on Zulip Jason KY. (Mar 28 2020 at 13:34):

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

view this post on Zulip Kenny Lau (Mar 28 2020 at 13:35):

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

view this post on Zulip Jason KY. (Mar 28 2020 at 13:36):

Alright, will do!

view this post on Zulip 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]

view this post on Zulip Kenny Lau (Mar 28 2020 at 13:40):

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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Reid Barton (Mar 28 2020 at 13:43):

Jason KY. said:

Kenny Lau said:

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

Sorry but what does idiomatic mean?

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

view this post on Zulip Kenny Lau (Mar 28 2020 at 13:44):

Jason KY. said:

Kenny Lau said:

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

Sorry but what does idiomatic mean?

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

view this post on Zulip Jason KY. (Mar 28 2020 at 13:44):

Ah, alright!

view this post on Zulip 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 idiomatic

Sorry but what does idiomatic mean?

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

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

view this post on Zulip Kenny Lau (Mar 28 2020 at 13:44):

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

view this post on Zulip Jason KY. (Mar 28 2020 at 13:46):

Right, I'll try to use finset.sup in the future then, thanks for the help!

view this post on Zulip Kenny Lau (Mar 28 2020 at 13:47):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (Mar 28 2020 at 13:47):

ok yes

view this post on Zulip 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) :=

view this post on Zulip Reid Barton (Mar 28 2020 at 13:48):

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

view this post on Zulip Kenny Lau (Mar 28 2020 at 13:48):

huh

view this post on Zulip Reid Barton (Mar 28 2020 at 13:48):

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

view this post on Zulip Jason KY. (Mar 28 2020 at 13:49):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Reid Barton (Mar 28 2020 at 13:56):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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,  ε : , ( : 0 < ε), open_ball s ε   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?)

view this post on Zulip Patrick Massot (Mar 29 2020 at 16:31):

I think you have too many commas.

view this post on Zulip Patrick Massot (Mar 29 2020 at 16:32):

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

view this post on Zulip Reid Barton (Mar 29 2020 at 16:32):

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

view this post on Zulip Reid Barton (Mar 29 2020 at 16:32):

is at least syntactically correct

view this post on Zulip Jason KY. (Mar 29 2020 at 16:33):

Ah, I see! thanks!

view this post on Zulip 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.

view this post on Zulip Jason KY. (Mar 29 2020 at 16:35):

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

view this post on Zulip Patrick Massot (Mar 29 2020 at 16:36):

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

view this post on Zulip Jason KY. (Mar 29 2020 at 16:37):

Why would it be a bad idea with these constraints?

view this post on Zulip Patrick Massot (Mar 29 2020 at 16:40):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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,  (ε : ) ( : 0 < ε), open_ball s ε  S

view this post on Zulip Jason KY. (Mar 29 2020 at 16:50):

But I guess it doesn't really matter either way

view this post on Zulip Patrick Massot (Mar 29 2020 at 16:50):

I would keep the natural writing order here.

view this post on Zulip Kevin Buzzard (Mar 29 2020 at 17:17):

Oh! There are cases when >is OK?

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Mar 29 2020 at 17:28):

You can always plea the linter's indulgence.

view this post on Zulip Patrick Massot (Mar 29 2020 at 17:29):

with @[nolint ge_or_gt]

view this post on Zulip 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,  (ε : ) ( : 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?

view this post on Zulip 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

view this post on Zulip Jason KY. (Mar 31 2020 at 18:35):

Thank you so much Alex!

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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,  (ε : ) ( : 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?

view this post on Zulip Reid Barton (Apr 04 2020 at 17:36):

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

view this post on Zulip Jason KY. (Apr 04 2020 at 17:40):

Is the statement bad because of the squiggly brackets or because of the Type*s?

view this post on Zulip Reid Barton (Apr 04 2020 at 17:41):

The Type*s

view this post on Zulip Reid Barton (Apr 04 2020 at 17:41):

You should replace those with an arbitrary type

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Reid Barton (Apr 04 2020 at 17:57):

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

view this post on Zulip Jason KY. (Apr 04 2020 at 17:58):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Apr 04 2020 at 18:12):

did you try simp?

view this post on Zulip Mario Carneiro (Apr 04 2020 at 18:12):

that's the sort of thing that simp is likely to know

view this post on Zulip Jason KY. (Apr 04 2020 at 18:13):

Just tried it, doesn't work :/

view this post on Zulip 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

view this post on Zulip Jason KY. (Apr 04 2020 at 18:15):

Alright, I'll try it out!

view this post on Zulip 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'

view this post on Zulip 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₂

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 04 2020 at 18:22):

if you reuse the variable it will be {α : Type*} which doesn't apply to Prop

view this post on Zulip Jason KY. (Apr 04 2020 at 18:25):

So {α} is just short for {α : Sort*}?

view this post on Zulip 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

view this post on Zulip Jason KY. (Apr 04 2020 at 18:30):

Ah, I see. Thank you!


Last updated: May 14 2021 at 02:15 UTC