## Stream: new members

### Topic: spheres

#### Greg Langmead (Jan 29 2020 at 14:58):

I am trying to construct unit n-spheres and prove they are smooth manifolds. I'm stuck at proving that stereographic projection is continuous. The chat room has already helped me prove continuity of a similar function on a subset of ℝ×ℝ (over in 'noob questions') but adding fin to the mix has me lost again. The function now has two arguments: a point on the sphere and the fin from the codomain of euclidean space, hence continuous.mul does not apply directly ("does not unify"). (Meta: I feel like I'm lacking some general principles to get myself unstuck in these situations!)

import geometry.manifold.real_instances

noncomputable theory

-- note: def euclidean_space (n : ℕ) : Type := (fin n → ℝ)

-- Unit sphere of dimension n, inside euclidean space of dimension n + 1
def unit_sphere (n : ℕ) := { x : euclidean_space (n + 1) // finset.univ.sum (λ i, (x i) ^ 2) = 1}
instance sphere_top_space (n : ℕ) : topological_space (unit_sphere n) := subtype.topological_space
instance sphere_has_coe_to_euclidean_space (n : ℕ) : has_coe (unit_sphere n) (euclidean_space (n + 1)) := coe_subtype

-- The unit sphere minus its north pole will be a coordinate chart via stereographic projection
def unit_sphere_minus_north_pole (n : ℕ) := { x : unit_sphere n // ((x : (euclidean_space (n + 1))) n) ≤ 1 }
instance sphere_minus_np_top_space (n : ℕ) : topological_space (unit_sphere_minus_north_pole n) := subtype.topological_space
instance sphere_minus_np_has_coe_to_sphere (n : ℕ) : has_coe (unit_sphere_minus_north_pole n) (unit_sphere n) := coe_subtype
instance sphere_minus_np_has_coe_to_euclidean_space (n : ℕ) : has_coe (unit_sphere_minus_north_pole n) (euclidean_space (n + 1)) := sorry

def stereographic_projection_north (n : ℕ) : (unit_sphere_minus_north_pole (n + 1)) → (euclidean_space (n + 1)) :=
λ sphere i, ((sphere : euclidean_space (n + 2)) i) * (1 - ((sphere : euclidean_space (n + 2)) (n + 1)))⁻¹

lemma continuous_sp_north (n:ℕ) : continuous (stereographic_projection_north n) :=
begin
unfold stereographic_projection_north,
apply continuous.mul, -- fails to unify
end


#### Sebastien Gouezel (Jan 29 2020 at 16:51):

Currently, there is only one explicit example of a smooth manifold in mathlib. It is the closed interval, endowed with a manifold with boundary structure, in the file real_instances.lean. You could take this as an example to see how things go. To define a smooth manifold structure, you need two things: an atlas (i.e., a set of local homeomorphisms between parts of your space and parts of euclidean space), and then a proof that the change of coordinates of member of this atlas are smooth. So, the first thing you need is the atlas.

An atlas is made of local homeos, called charts. For the closed interval, the first chart is defined at https://github.com/leanprover-community/mathlib/blob/b36831204c0db0c18b35918b56ffd3df55707c9e/src/geometry/manifold/real_instances.lean#L202 . There, you can see that there is a subtlety in the definition of local homeos: to avoid subtype problems that you are running into, they are not defined on subtypes of the space, but on subsets (and then the function defining your local homeo is defined everywhere, not only on your subset, but the values outside of it are just garbage). So, you should change your code to define unit_sphere_minus_north_pole as a subset of the sphere (which means that you can avoid some instances you are declaring). Of course, the functions will only be continuous on the subset where they make sense, which means that you will use continuous_on instead of continuous in most your proofs.

Here is a skeleton of what your construction might look like, with a lot of sorries that you would need to fill in:

variable (n : ℕ)

def unit_sphere := {x : euclidean_space (n + 1) // finset.univ.sum (λ i, (x i) ^ 2) = 1}
instance sphere_top_space : topological_space (unit_sphere n) := subtype.topological_space
instance sphere_has_coe_to_euclidean_space : has_coe (unit_sphere n) (euclidean_space (n + 1)) := coe_subtype

-- The unit sphere minus its north pole will be a coordinate chart via stereographic projection
def unit_sphere_minus_north_pole (n : ℕ) : set (unit_sphere n) :=
{x | (x : (euclidean_space (n + 1))) n < 1}

def stereographic_projection_north_local_equiv : local_equiv (unit_sphere n) (euclidean_space n) :=
{ source := unit_sphere_minus_north_pole n,
target := univ,
to_fun := λ sphere, (λi, ((sphere : euclidean_space (n + 1)) i) * (1 - ((sphere : euclidean_space (n + 1)) (n + 1)))⁻¹),
inv_fun := λx, sorry, -- put the formula for the element of the sphere which is the inverse of
-- x under the stereographic projection
map_source := sorry, -- all these fields say that the functions to_fun and inv_fun are inverse
map_target := sorry, -- to each other on the sets source and target
left_inv := sorry,
right_inv := sorry }

def stereographic_projection_north : local_homeomorph (unit_sphere n) (euclidean_space n) :=
{
..stereographic_projection_north_local_equiv n }


If you put your cursor in vscode on the opening brace of stereographic_projection_north, you will see that there are fields in local_homeomorph that I have not mentioned but that need filling (i.e., open_source, open_target, continuous_to_fun, continuous_inv_fun). But before trying to do the continuity proofs, I think you should try to complete the definition of the local equivalence, i.e., give the formula for the inverse of the stereographic projection and check that you indeed have a bijection.

#### Yury G. Kudryashov (Jan 29 2020 at 17:25):

BTW, why do we need the atlas? Why not say "for any point its chart satisfies" instead of "for any member of the atlas"?

#### Sebastien Gouezel (Jan 29 2020 at 17:44):

Right now, we have an atlas, and for each point x in the manifold we have a chosen member of the atlas that contains x in its domain, and that we call chart_at x. We could definitely replace the atlas by the set of all chart_at x for x in the manifold, and it wouldn't change anything (essentially no gain or no loss from what I could tell). The usual math approach is to have an atlas, though, so I decided to stick with it just for familiarity reasons.

#### Patrick Massot (Jan 29 2020 at 18:04):

Let me write once again that our current definition of manifold is nothing familiar to mathematicians, and should be called charted_space so I'd be open to modifying the definition if Yuri thinks it would make things simpler.

#### Sebastien Gouezel (Jan 29 2020 at 18:10):

I would agree to rename it charted_space. But still, I would keep the atlas to help mathematicians.

#### Johan Commelin (Jan 29 2020 at 18:55):

Will that change implicitly mean that there will typically be infinitely many charts?

#### Johan Commelin (Jan 29 2020 at 18:56):

If so, I would prefer to keep the atlas. For some definitions it is important to have a finite atlas.

#### Sebastien Gouezel (Jan 29 2020 at 19:36):

Many points can have the same chart, so no it does not imply that there are typically infinitely many charts. But in any case this kind of discussion is easier to do with the atlas, so this is one more reason to keep it.

#### Yury G. Kudryashov (Jan 29 2020 at 22:42):

Then I propose to add a constructor setting atlas to be there range of chart_at

#### Yury G. Kudryashov (Jan 29 2020 at 23:52):

@Patrick Massot Is it not "manifold" because we fix the best chart for each point or because of something else?

#### Yury G. Kudryashov (Jan 30 2020 at 03:12):

Then I propose to add a constructor setting atlas to be there range of chart_at

#### Patrick Massot (Jan 30 2020 at 08:25):

The best chart function is a tiny implementation detail that is not visible in the real world where we simply choose a chart whenever we need one. The reason mathlib manifold is not a manifold structure is much deeper. There is no maximality condition on the atlas (and no equivalence class of atlases). Adding a compatible chart to a mathlib manifold gives you a new manifold.

#### Yury G. Kudryashov (Jan 30 2020 at 08:41):

The best chart function contributes to this.

#### Greg Langmead (Jan 30 2020 at 13:20):

If a smooth manifold is a topological manifold together with its atlas then you do get a new one by adding a compatible chart, but of course they are diffeomorphic. Sometimes we have some equivalence class in mind and this detail is a distraction. Could Lean's quotients help define the equivalence class in a way that lets us work in both approaches? (Having a multiplicity of approaches feels right to me -- many equivalent definitions and proofs that they are equivalent.)

#### Greg Langmead (Feb 07 2020 at 00:59):

I took the suggestions of @Sebastien Gouezel, and have a new question. I'm defining the inverse of stereographic projection, the function that maps euclidean space of dimension n back into the sphere of dimension n, living in euclidean space of dimension n+1. The lambda doesn't typecheck -- where, in what structure, do I provide the proof that the image of this map is in fact contained in the sphere?

def unit_sphere_minus_north_pole (n) : set (unit_sphere n) :=
{x | (x : (euclidean_space (n + 1))) n < 1}

def stereographic_projection_inv_north (n) : (euclidean_space n) → (unit_sphere n) :=
λx, (λ(i : fin (n + 1)), if lt : i.val < n
then 2 * (x (fin_upgrade n i lt)) / (1 + finset.univ.sum (λ i, (x i) ^ 2))
else (-1 + finset.univ.sum (λ i, (x i) ^ 2)) / (1 + finset.univ.sum (λ i, (x i) ^ 2)))


This doesn't typecheck, it says

type mismatch, term
λ (x : euclidean_space n) (i : fin (n + 1)),
dite (i.val < n)
(λ (lt : i.val < n), 2 * x (fin_upgrade n i lt) / (1 + finset.sum finset.univ (λ (i : fin n), x i ^ 2)))
(λ (lt : ¬i.val < n),
(-1 + finset.sum finset.univ (λ (i : fin n), x i ^ 2)) /
(1 + finset.sum finset.univ (λ (i : fin n), x i ^ 2)))
has type
euclidean_space n → fin (n + 1) → ℝ
but is expected to have type
euclidean_space n → unit_sphere n


#### Mario Carneiro (Feb 07 2020 at 02:44):

unit_sphere is a subtype, right? So you need to have a proof after it:

def stereographic_projection_inv_north (n) : (euclidean_space n) → (unit_sphere n) :=
λx, ⟨λ(i : fin (n + 1)), if lt : i.val < n
then 2 * (x (fin_upgrade n i lt)) / (1 + finset.univ.sum (λ i, (x i) ^ 2))
else (-1 + finset.univ.sum (λ i, (x i) ^ 2)) / (1 + finset.univ.sum (λ i, (x i) ^ 2)),
sorry⟩


#### Greg Langmead (Feb 07 2020 at 02:52):

Yes unit_sphere is a subtype

def unit_sphere (n) := { x : euclidean_space (n + 1) // finset.univ.sum (λ i, (x i) ^ 2) = 1}


I added the sorry and it's a variation on the above error, but this gives me something to follow up on so I'll keep at it, thanks!

#### Greg Langmead (Feb 18 2020 at 13:46):

Currently I am trying to supply the proof that the inverse of stereographic projection lands in the sphere, but because it's a summation I don't know what sort of tools to use. The new hint tactic lists a few tactics that make progress but it's not really actionable since I can't assemble them into a proof so far. Am I looking for a combination of standard tactics like field_simp/norm_num/ring or is something additional needed due to the sum?

And as a meta-question, what techniques am I missing that would enable me to understand at least a sketch of what I need to do next? My only methods are to try a few tactics I know and see if they magically work. I don't know how to incrementally build something.

import geometry.manifold.real_instances
import tactic.hint

noncomputable theory

variable (n : ℕ)

def fin_upgrade (n) (i : fin (n + 1)) (lt : i.val < n) : (fin n) := {
val := i.val,
is_lt := lt
}

-- Unit sphere of dimension n, inside euclidean space of dimension n + 1
def unit_sphere (n) := { x : euclidean_space (n + 1) // finset.univ.sum (λ i, (x i) ^ 2) = 1}

def stereographic_projection_inv_north (n) : (euclidean_space n) → (unit_sphere n) :=
λx, ⟨λ(i : fin (n + 1)), (if lt : i.val < n
then (2 * (x (fin_upgrade n i lt)) / (finset.univ.sum (λ j, (x j) ^ 2) + 1))
else (((finset.univ.sum (λj, (x j)^2) - 1) / (finset.univ.sum (λ j, (x j)^2) + 1)))),
begin
sorry,
-- hint recommends: ring, norm_num, simp at *, dsimp at *
end
⟩


#### Kevin Buzzard (Feb 18 2020 at 13:52):

I would not take what hint recommends too seriously. It's supposed to be used for "simple" problems, and if you think this is simple then you're miscalibrated.

#### Kevin Buzzard (Feb 18 2020 at 13:55):

Looking at what you have, it seems to me that the first step is to break up the sum from 0 to n as a sum from 0 to n-1, plus the n'th term. This will enable you to get rid of the "if". Then you want to take the division outside the sum.

#### Kevin Buzzard (Feb 18 2020 at 13:58):

Then the question should become a question in ring theory, and you'll still have some work to do. But step 1 should be getting rid of the if and step 2 getting rid of the denominators.

#### Kevin Buzzard (Feb 18 2020 at 14:17):

finset.sum_range_succ :
∀ (f : ℕ → ?M_1) (n : ℕ), finset.sum (finset.range (nat.succ n)) f = f n + finset.sum (finset.range n) f

finset.sum_mul : finset.sum ?M_3 ?M_4 * ?M_5 = finset.sum ?M_3 (λ (x : ?M_1), ?M_4 x * ?M_5)

div_eq_mul_inv : ?M_3 / ?M_4 = ?M_3 * ?M_4⁻¹


#### Kevin Buzzard (Feb 18 2020 at 14:32):

This is kind of annoying because you don't have f : ℕ → ?M_1, you have f : fin n → ℝ

#### Greg Langmead (Feb 18 2020 at 15:19):

I'm not clear how I can get rid of the if. The codomain of this function is unit_sphere n which is in R^(n+1), so I need a lambda on fin (n + 1) which has two cases with different formulas. Here's the formula from R^2 to R^3:
pasted image
Once I have the function I need to prove its values have norm 1. Does Lean know that I should sum the square of all the cases of the if? Could I express the function in the first place as being divided by its own norm? Ooh maybe I should break this up into the composition of two functions: a nonzero function followed by dividing that function by its own norm.

#### Kevin Buzzard (Feb 18 2020 at 16:14):

Right. So your job is to prove that the sum of the squares of those entries is 1. My proposal is to write the sum as (the sum of the first $n$ things) plus (the last thing), then take out the factor $1+\sum_{i=0}^{n-1}X_i^2$, then you're reduced to proving $(-1+\sum_{i=0}^{n-1}X_i^2)^2+\sum_{i=0}^{n-1}(2X_i)^2=(1+\sum_{i=0}^{n-1}(X_i)^2)^2$, which you can do using $(a+b)^2=a^2+b^2+2ab$.

#### Kevin Buzzard (Feb 18 2020 at 18:16):

import geometry.manifold.real_instances

noncomputable theory

variable (n : ℕ)

def fin_upgrade (n) (i : fin (n + 1)) (lt : i.val < n) : (fin n) := {
val := i.val,
is_lt := lt
}

theorem finset.sum_univ_fin_eq_sum_range (n : ℕ) (f : fin n → ℝ) :
finset.sum finset.univ f = (finset.range n).sum (λ i, if hi : i < n then f ⟨i, hi⟩ else 0) :=
begin
set F : ℕ → ℝ := λ i, if hi : i < n then f ⟨i, hi⟩ else 0 with hF,
have H : f = λ (i : fin n), F (i.val),
{ ext i,
rw hF,
show f i = dite (i.val < n) (λ (hi : i.val < n), f ⟨i.val, hi⟩) (λ (hi : ¬i.val < n), 0),
rw dif_pos i.is_lt,
cases i, refl,
},
rw H,
rw ←finset.sum_image,
{ congr',
-- ⊢ finset.image (λ (x : fin n), x.val) finset.univ = finset.range n
ext j, -- sigh
rw [finset.mem_range, finset.mem_image],
split,
rintro ⟨⟨j,hj⟩, _, rfl⟩,
exact hj,
intro hj,
use ⟨j, hj⟩,
split, apply finset.mem_univ, refl
},
intros _ _ _ _,
exact fin.eq_of_veq,
end

theorem finset.sum_div {α : Type*} {s : finset α} (f : α → ℝ) (d : ℝ) : finset.sum s (λ a, f a / d) = finset.sum s f / d :=
begin
by_cases hd : d = 0,
rw [hd, div_zero],
convert finset.sum_const_zero,
ext _,
rw div_zero,
rw [div_eq_mul_inv, finset.sum_mul],
congr',
end

def unit_sphere (n) := { x : euclidean_space (n + 1) // finset.univ.sum (λ i, (x i) ^ 2) = 1}

open finset

def stereographic_projection_inv_north (n) : (euclidean_space n) → (unit_sphere n) :=
λx, ⟨λ(i : fin (n + 1)), (if lt : i.val < n
then (2 * (x (fin_upgrade n i lt)) / (finset.univ.sum (λ j, (x j) ^ 2) + 1))
else (((finset.univ.sum (λj, (x j)^2) - 1) / (finset.univ.sum (λ j, (x j)^2) + 1)))),
begin
rw [sum_univ_fin_eq_sum_range, sum_range_succ, dif_pos (nat.lt_succ_self n), dif_neg (lt_irrefl n)],
suffices : ((sum univ (λ (j : fin n), x j ^ 2) - 1) / (sum univ (λ (j : fin n), x j ^ 2) + 1)) ^ 2 +
(sum (range n) (λ (i : ℕ), if hi : i < n then (2 * x ⟨i, hi⟩)^2  else 0) / (sum univ (λ (j : fin n), x j ^ 2) + 1) ^ 2)
= 1,
{ convert this using 2, clear this,
rw ←sum_div,
apply finset.sum_congr, refl,
intros i hi,
rw finset.mem_range at hi,
rw dif_pos (lt_trans hi (nat.lt_succ_self n)),
rw dif_pos hi,
rw dif_pos hi,
rw pow_div,
congr',
},
rw pow_div,
rw div_eq_one_iff_eq,
swap, sorry, -- (sum univ (λ (j : fin n), x j ^ 2) + 1) ^ 2 ≠ 0
rw [neg_mul_neg, mul_neg_one, mul_one, mul_one],
congr' 1,
apply congr_arg,
rw sum_univ_fin_eq_sum_range,
apply sum_congr, refl,
intros i hi,
rw mem_range at hi,
rw [dif_pos hi, dif_pos hi],
ring,
end
⟩


One sorry left: I need that $1+X^2+Y^2\not=0$ otherwise the result is false. Hang on...

#### Patrick Massot (Feb 18 2020 at 18:24):

example (x y : ℝ) : 1 + x^2 + y^2 ≠ 0 :=
by linarith [pow_two_nonneg x, pow_two_nonneg y]


#### Kevin Buzzard (Feb 18 2020 at 18:25):

yeah but it's a sum over fin n really. I've done it, I'm just editing.

#### Kevin Buzzard (Feb 18 2020 at 18:26):

Aren't you proud of sum_div? I didn't need d non-zero :-) However I needed it later on anyway :-(

#### Kevin Buzzard (Feb 18 2020 at 18:27):

import geometry.manifold.real_instances

noncomputable theory

variable (n : ℕ)

def fin_upgrade (n) (i : fin (n + 1)) (lt : i.val < n) : (fin n) := {
val := i.val,
is_lt := lt
}

theorem finset.image_val_univ_eq_range (n : ℕ) : finset.image (λ (x : fin n), x.val) finset.univ = finset.range n :=
begin
ext j, -- sigh
rw [finset.mem_range, finset.mem_image],
split,
rintro ⟨⟨j,hj⟩, _, rfl⟩,
exact hj,
intro hj,
use ⟨j, hj⟩,
split, apply finset.mem_univ, refl
end

theorem finset.sum_univ_fin_eq_sum_range (n : ℕ) (f : fin n → ℝ) :
finset.sum finset.univ f = (finset.range n).sum (λ i, if hi : i < n then f ⟨i, hi⟩ else 0) :=
begin
set F : ℕ → ℝ := λ i, if hi : i < n then f ⟨i, hi⟩ else 0 with hF,
have H : f = λ (i : fin n), F (i.val),
{ ext i,
rw hF,
show f i = dite (i.val < n) (λ (hi : i.val < n), f ⟨i.val, hi⟩) (λ (hi : ¬i.val < n), 0),
rw dif_pos i.is_lt,
cases i, refl,
},
rw H,
rw ←finset.sum_image,
{ congr',
apply finset.image_val_univ_eq_range,
},
intros _ _ _ _,
exact fin.eq_of_veq,
end

theorem finset.sum_div {α : Type*} {s : finset α} (f : α → ℝ) (d : ℝ) : finset.sum s (λ a, f a / d) = finset.sum s f / d :=
begin
by_cases hd : d = 0,
rw [hd, div_zero],
convert finset.sum_const_zero,
ext _,
rw div_zero,
rw [div_eq_mul_inv, finset.sum_mul],
congr',
end

def unit_sphere (n) := { x : euclidean_space (n + 1) // finset.univ.sum (λ i, (x i) ^ 2) = 1}

open finset

def stereographic_projection_inv_north (n) : (euclidean_space n) → (unit_sphere n) :=
λx, ⟨λ(i : fin (n + 1)), (if lt : i.val < n
then (2 * (x (fin_upgrade n i lt)) / (finset.univ.sum (λ j, (x j) ^ 2) + 1))
else (((finset.univ.sum (λj, (x j)^2) - 1) / (finset.univ.sum (λ j, (x j)^2) + 1)))),
begin
rw [sum_univ_fin_eq_sum_range, sum_range_succ, dif_pos (nat.lt_succ_self n), dif_neg (lt_irrefl n)],
suffices : ((sum univ (λ (j : fin n), x j ^ 2) - 1) / (sum univ (λ (j : fin n), x j ^ 2) + 1)) ^ 2 +
(sum (range n) (λ (i : ℕ), if hi : i < n then (2 * x ⟨i, hi⟩)^2  else 0) / (sum univ (λ (j : fin n), x j ^ 2) + 1) ^ 2)
= 1,
{ convert this using 2, clear this,
rw ←sum_div,
apply finset.sum_congr, refl,
intros i hi,
rw finset.mem_range at hi,
rw dif_pos (lt_trans hi (nat.lt_succ_self n)),
rw dif_pos hi,
rw dif_pos hi,
rw pow_div,
congr',
},
rw pow_div,
rw div_eq_one_iff_eq,
swap,
{ apply ne_of_gt,
apply pow_pos,
apply lt_of_lt_of_le zero_lt_one,
apply sum_nonneg,
intros,
rw pow_two,
apply mul_self_nonneg,
},
rw [neg_mul_neg, mul_neg_one, mul_one, mul_one],
congr' 1,
apply congr_arg,
rw sum_univ_fin_eq_sum_range,
apply sum_congr, refl,
intros i hi,
rw mem_range at hi,
rw [dif_pos hi, dif_pos hi],
ring,
end
⟩


It looks to me like there are a couple of holes in the finset library, which made life a bit harder.

#### Kevin Buzzard (Feb 18 2020 at 18:30):

My Lean is rather amateurish at times, but I understand the system well enough to be able to muddle through. It would not surprise me at all if someone who knows how to code could halve the size of this code. There used to be something called the @Mario Carneiro ratio, where the game was that you wrote some code, and then Mario rewrote it, and your ratio was the number of lines of your code divided by the number of lines of his code. We mathematicians used to work on trying to get the ratio down below 5.

#### Patrick Massot (Feb 18 2020 at 18:46):

I haven't read the proof carefully, but clearly this is the opportunity to get some new sum lemmas. Maybe also use indicator?

#### Sebastien Gouezel (Feb 18 2020 at 20:13):

Kevin Buzzard said:

def fin_upgrade (n) (i : fin (n + 1)) (lt : i.val < n) : (fin n) := {
val := i.val,
is_lt := lt
}


This is called fin.cast_lt, I think.

#### Greg Langmead (Feb 18 2020 at 22:23):

Wow this is fantastic, huge thanks Kevin! I'll digest this post haste. @Sebastien Gouezel that fin_upgrade was mine, I didn't find fin.cast_lt. That's my ongoing problem. I neither know what steps Lean wants from me, nor how to find them when I happen to understand.

#### Kevin Buzzard (Feb 18 2020 at 22:35):

The rule is this: if it looks basic, it's there already. It might be heavily disguised (e.g. earlier today I was asking how to take a finite union of finite sets and it turns out that the answer has something to do with monads) but it will be there. The trick is working out what the right question is. If it's there, it might well have a fabulous API (e.g. checking that making each set bigger makes the union bigger might be just some crazy one line incomprehensible monad or filter proof, but it might also have a sensible name).

After a while you just realise exactly what the computer is asking you to do, and you become a precision user of the tools which are available to you. I just learnt by doing a wide range of mathematics at all levels and running into myriads of different problems and having them all solved for me by others here.

#### Kevin Buzzard (Feb 18 2020 at 22:38):

That code I posted earlier took me a couple of hours to write, but I never really got stuck. It would be great if a CS person could review it because then you might also be able to witness how the experts can write it in half the space and in a way which sometimes can be far far harder to understand.

#### Kevin Buzzard (Feb 18 2020 at 22:38):

All my proofs are in tactic mode and you can just step through them.

#### Kevin Buzzard (Feb 18 2020 at 22:40):

You can even step through the rewrites term by term, by clicking near the commas.

#### Daniel Keys (Feb 19 2020 at 03:52):

I have a statement that a set is non-empty and need to produce a statement that a member of that set exists. Something along this line:

variable {X  : Type u}
variable set1 : set X
variable nonEmptySetProp : ¬ (set1 = ∅)


and need to produce ∃ x, x ∈ set1. The only thing I can find in data/set/basic is set.exists_mem_of_nonempty which doesn't work here. Any idea how to proceed appreciated!

#### Alex J. Best (Feb 19 2020 at 03:58):

import data.set.basic

variable {X  : Type}
variable set1 : set X
variable nonEmptySetProp : ¬ (set1 = ∅)

example : ∃ a, a ∈ set1 :=
set.ne_empty_iff_nonempty.mp nonEmptySetProp


#### Alex J. Best (Feb 19 2020 at 03:59):

As of quite recently set1.nonempty which literally means ∃ a, a ∈ set1 is the preferred way of expressing the sentiment that s \ne \emptyset

#### Daniel Keys (Feb 19 2020 at 04:15):

This is exactly what I needed and I just realized I awkwardly posted in a totally unrelated topic. :upside_down:
I'll blame it on the late hour!

Last updated: May 16 2021 at 05:21 UTC