## 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 havebounded_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 idiomatic

Sorry 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 idiomatic

Sorry but what does idiomatic mean?

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

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 idiomatic

Sorry 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

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) :=


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