## Stream: new members

### Topic: member of cartesian product of sets

#### Ashwin Iyengar (Feb 17 2021 at 18:44):

I'm struggling to understand why this (contrived example) doesn't compile, I don't understand how sets work really:

import analysis.normed_space.basic

variables (S R : Type*) [normed_ring R]

lemma x (f : S → R) (r : set S × S) : true :=
begin
have : ∃ x ∈ r, ∥f x.1∥ = ∥f x.2∥ := sorry
end


#### Kevin Buzzard (Feb 17 2021 at 18:47):

I think this is just the Lean 3 parser giving up on you rather than any misunderstanding on your part.

#### Johan Commelin (Feb 17 2021 at 18:48):

lemma x (f : S → R) (r : set (S × S)) : true :=
begin
have : ∃ (x : S × S) (hx : x ∈ r), ∥f x.1∥ = ∥f x.2∥ := sorry
end


#### Johan Commelin (Feb 17 2021 at 18:48):

Note that you had another problem. Lean parses the type of r as (set S) × S

#### Ashwin Iyengar (Feb 17 2021 at 18:50):

Oh I see, so the point is that membership is a proposition?

yes

Cool thanks

#### Kevin Buzzard (Feb 17 2021 at 18:50):

#print notation × -- _ ×:35 _:34 := prod #1 #0 -- \times has a meagre binding power of 35, and set is a function so has a binding power of something like 1000.

#### Ashwin Iyengar (Feb 17 2021 at 19:03):

Hm okay does this nonarchimedean_normed_ring.ultrametric look like a reasonable statement then? It compiles but I'm not sure I'm using everything correctly.

import analysis.normed_space.basic
import ring_theory.power_series.basic

open filter

noncomputable theory
open_locale big_operators

class nonarchimedean_normed_ring (R : Type*) extends normed_ring R :=
(ultrametric_inequality : ∀ x y : R, ∥x + y∥ ≤ (max ∥x∥ ∥y∥))

variables {R : Type*} [normed_ring R]

lemma nonarchimedean_normed_ring.ultrametric {S : set R} {t : finset S} {n : nonempty S} (m: S → R) :
∃ x : S, ∥∑ p in t, m p∥ ≤ ∥m x∥ ∧ ∀ y : S, ∥m y∥ ≤ ∥m x∥ :=
begin
sorry
end


#### Kevin Buzzard (Feb 17 2021 at 19:04):

Functions seem to have binding power 1024 by the way:

variables (f : ℕ → ℤ) (a b : ℕ)

def moo : ℕ → ℕ → ℕ := λ a b, 0

notation a ★:1025 b := moo a b -- will fail if you lower this to 1024

#check f a ★ b -- works


#### Johan Commelin (Feb 17 2021 at 19:06):

For exactly this reason of binding powers, you shouldn't need () around max here:

(ultrametric_inequality : ∀ x y : R, ∥x + y∥ ≤ (max ∥x∥ ∥y∥))


#### Johan Commelin (Feb 17 2021 at 19:07):

The lemma statement looks a bit non-idiomatic too me...

#### Johan Commelin (Feb 17 2021 at 19:09):

I would replace {S : set R} by {S : Type*}

#### Johan Commelin (Feb 17 2021 at 19:09):

And use [nonempty S]

#### Kevin Buzzard (Feb 17 2021 at 19:09):

I'm not sure it's true as it stands. What about if S is infinite, m is unbounded, and t is empty?

#### Kevin Buzzard (Feb 17 2021 at 19:10):

And also what Johan says -- S doesn't need to be anything to do with R. I think you want that t is nonempty.

#### Ashwin Iyengar (Feb 17 2021 at 19:10):

Sorry I'm confused, basically there should only be S, I wanted t to be a proof that S is finite, but I think I'm misinterpreting what a finset is

#### Kevin Buzzard (Feb 17 2021 at 19:11):

t : finset S means t is a finite subset of S. Maybe you want hS : S.finite then

#### Kevin Buzzard (Feb 17 2021 at 19:11):

except that because you don't even need S to be a set, you maybe want a random nonempty finite type S.

#### Kevin Buzzard (Feb 17 2021 at 19:12):

lemma nonarchimedean_normed_ring.ultrametric {ι : Type*} [fintype ι]
[nonempty ι] (m: ι → R) :
∃ x : ι, ∥∑ p, m p∥ ≤ ∥m x∥ ∧ ∀ y : ι, ∥m y∥ ≤ ∥m x∥ :=
begin
sorry
end


hopefully that's true.

#### Johan Commelin (Feb 17 2021 at 19:13):

But actually, the version with s : finset \iota will probably be more useful in practice.

#### Kevin Buzzard (Feb 17 2021 at 19:14):

set S is the type of subsets of S, finset S is the type of finite subsets of S, set.finite is a predicate on set S saying "I am finite", fintype is a predicate on Type saying "I am finite".

#### Johan Commelin (Feb 17 2021 at 19:14):

So the I would drop the [fintype \iota], replace [nonempty \iota] by (hs : s.nonempty) and \ex x : \iota by \ex x \in s.

#### Kevin Buzzard (Feb 17 2021 at 19:14):

with s : finset iota

#### Kevin Buzzard (Feb 17 2021 at 19:17):

I totally agree that this is confusing and that there is no obvious reference to point to.

#### Ashwin Iyengar (Feb 17 2021 at 19:18):

Thanks that clarifies things! Then this gives an error still

lemma nonarchimedean_normed_ring.ultrametric {ι : Type*} {S : finset ι} (hS : S.nonempty) (m : S → R) :
∃ x ∈ S, ∥∑ p, m p∥ ≤ ∥m x∥ ∧ ∀ y ∈ S, ∥m y∥ ≤ ∥m x∥ :=
begin
sorry
end


#### Ashwin Iyengar (Feb 17 2021 at 19:18):

Apparently I can't make a map out of a finset... I guess it's not a type

#### Kevin Buzzard (Feb 17 2021 at 19:18):

Maybe you want m : iota -> R

#### Ashwin Iyengar (Feb 17 2021 at 19:19):

But then presumably m has to be defined on all of \iota, when I would just want it to be defined on S

#### Kevin Buzzard (Feb 17 2021 at 19:19):

S : finset iota is a term not a type, it has type finset iota. Types have type Type. But clearly you sometimes want to think of S as a type in itself, the type of elements of S, so there is a way to coerce it into a type, but it involves up-arrows because nobody fixed it yet.

#### Kevin Buzzard (Feb 17 2021 at 19:21):

If you only want m to be defined on S then you could go with my [fintype iota] suggestion. But Johan's point is that actually if you think you have a map defined only on S, you might well find that Lean will happily let it be defined on all of iota, even if it involves things like division by 0, because this is some type theory philosophy that maps should be defined on all of a type and return junk values away from the domain of interest.

#### Kevin Buzzard (Feb 17 2021 at 19:21):

If you really only want m defined on S then there's no point having iota.

#### Kevin Buzzard (Feb 17 2021 at 19:22):

1/0=0, sup of the naturals in the reals is 0, as is sup of the empty set etc.

#### Kevin Buzzard (Feb 17 2021 at 19:22):

if you're foolish enough to give a set to the real.sup function which isn't non-empty and bounded, you'll get a junk answer rather than an error.

#### Johan Commelin (Feb 17 2021 at 19:23):

Ashwin Iyengar said:

Apparently I can't make a map out of a finset... I guess it's not a type

S : finset \iota means that S has type finset \iota. S : Type means that S has type Type. The latter means "S is a type". So indeed, finsets aren't types.
It takes a bit of time to get used to, but really everything only has 1 type.

#### Kevin Buzzard (Feb 17 2021 at 19:23):

so similarly here you might think that m is only defined on S but probably it will make sense on all of iota.

#### Johan Commelin (Feb 17 2021 at 19:24):

@Ashwin Iyengar for proofs it will be extremely convenient to have m defined on all of \iota, but also have s around as finset.

#### Johan Commelin (Feb 17 2021 at 19:24):

It means that you can restrict the sum to a smaller finset, or do induction on the size of the finset, and all the while m : \iota \to R doesn't change.

#### Johan Commelin (Feb 17 2021 at 19:25):

Thousands of lines of code about \sum x in s, m s have shown that this model is extremely convenient to work with in practice.

#### Ashwin Iyengar (Feb 17 2021 at 19:25):

Okay thanks. Final question, do you imagine that

lemma nonarchimedean_normed_ring.ultrametric {S : finset R} (hS : S.nonempty):
∃ x ∈ S, ∥∑ p in S, p∥ ≤ ∥x∥ ∧ ∀ y ∈ S, ∥y∥ ≤ ∥x∥


would be less useful than

lemma nonarchimedean_normed_ring.ultrametric {ι : Type*} {S : finset ι} (hS : S.nonempty) (m : ι → R) :
∃ x ∈ S, ∥∑ p in S, m p∥ ≤ ∥m x∥ ∧ ∀ y ∈ S, ∥m y∥ ≤ ∥m x∥


sure

#### Kevin Buzzard (Feb 17 2021 at 19:27):

the first is a trivial special case of the second, where two random types are being randomly decreed to be equal despite having nothing to do with each other.

#### Kevin Buzzard (Feb 17 2021 at 19:27):

Even if you have a type which you are convinced is equal to R (e.g. a type canonically isomorphic to R), Lean might not let you prove that it's equal to R.

#### Kevin Buzzard (Feb 17 2021 at 19:28):

Oh I see, you removed m too.

#### Johan Commelin (Feb 17 2021 at 19:28):

I would certainly go for the second version

#### Kevin Buzzard (Feb 17 2021 at 19:28):

I would still prove the second.

#### Johan Commelin (Feb 17 2021 at 19:29):

The proof will be just as long as that of the first, but it will be much easier to apply the second version

#### Ashwin Iyengar (Feb 17 2021 at 19:29):

Okay thanks, maybe to convince myself I'll compare how hard it is to apply the first one vs the second one in my proof that you can multiply restricted power series

#### Johan Commelin (Feb 17 2021 at 19:29):

(Note that when you apply the second version, usually lean will figure out automatically what \iota and m are. But with the first version you will hit situations quickly where you want to apply it, but lean will say "nope")

#### Kevin Buzzard (Feb 17 2021 at 19:41):

Ashwin, if you think that $R[1/fg]=R[1/f][1/g]$ then your notion of what equality is is not the same as Lean's. If you think you have elements of $R$ and they're actually elements of a ring canonically isomorphic to $R$ then you need the map. Experience has shown us that having an index type is a powerful level of abstraction which covers essentially all use cases.

#### Kevin Buzzard (Feb 17 2021 at 19:42):

If you really are in the situation where your map is not defined on all of iota, which does occasionally happen, then you just promote S to a type and continue anyway.

#### Ashwin Iyengar (Feb 17 2021 at 21:20):

Johan Commelin said:

For exactly this reason of binding powers, you shouldn't need () around max here:

(ultrametric_inequality : ∀ x y : R, ∥x + y∥ ≤ (max ∥x∥ ∥y∥))


Oh btw it doesn't work without the () for some reason

#### Ashwin Iyengar (Feb 17 2021 at 21:21):

≤ seems to take priority over the application of max or something