# Zulip Chat Archive

## Stream: maths

### Topic: Index of intersection

#### Ashvni Narayanan (Mar 22 2021 at 21:19):

I am trying to prove :

```
lemma Inter_nonempty_of' {α β : Type*} {ι : set β} {s : ι → set α} :
(⋂ j, s j).nonempty → nonempty ι :=
```

I don't actually need the assumption `{ι : set β}`

, but I am trying to use the lemma `set.not_nonempty_iff_eq_empty`

, since I can't think of any way to prove it apart from `contrapose`

.

Any help is appreciated, thank you!

#### Yury G. Kudryashov (Mar 22 2021 at 21:33):

Untested:

```
lemma Inter_nonempty_of' {α ι : Type*} {s : ι → set α} :
(⋂ j, s j).nonempty → nonempty ι :=
begin
rintro ⟨x, hx⟩,
rw mem_Union at hx,
rcases hx with ⟨j, hj⟩,
exact ⟨j⟩
end
```

AFAIR we have a lemma `∃ x : α, p x → nonempty α`

but I forgot the name.

#### Ashvni Narayanan (Mar 22 2021 at 21:41):

Thanks, @Yury G. Kudryashov ! The `rcases`

line gives the following error:

```
rcases tactic failed: hx : [anonymous] is not an inductive datatype
```

And I believe the lemma you mentioned is called `nonempty_of_exists`

.

#### Kevin Buzzard (Mar 22 2021 at 21:46):

I don't think this lemma is true. An empty intersection of subsets of X is just X.

#### Adam Topaz (Mar 22 2021 at 21:48):

But it's true if you replace intersection with union

#### Kevin Buzzard (Mar 22 2021 at 21:50):

```
import tactic
open set
lemma not_Inter_nonempty_of' : ¬ (∀ (α β : Type) (ι : set β) (s : ι → set α),
(⋂ j, s j).nonempty → nonempty ι) :=
begin
intro h,
specialize h ℕ ℕ ∅ (λ _, {37}) ⟨37, by simp⟩,
rcases h with ⟨⟨_, ⟨⟩⟩⟩,
end
```

#### Ashvni Narayanan (Mar 22 2021 at 21:53):

Yes, that makes sense, thank you!

#### Adam Topaz (Mar 22 2021 at 21:53):

Oh, it would be cool if slim check could find the "obvious" counter example. But I guess slim check can't generate random types?

#### Patrick Massot (Mar 22 2021 at 21:54):

It could tried a couple of finite types.

#### Adam Topaz (Mar 22 2021 at 21:56):

Actually now I can't even get slim check to generate a random natural number. What import am I missing?

```
import tactic.slim_check
example : ℕ := by slim_check
```

#### Kevin Buzzard (Mar 22 2021 at 21:57):

```
import tactic.slim_check
#sample nat
/-
0
1
6
1
1
0
6
212
7
9
-/
```

so it ~~should work~~ should be possible to make it to work...

#### Adam Topaz (Mar 22 2021 at 22:00):

Oh, the `slim_check.testable`

class is only for props

#### Adam Topaz (Mar 22 2021 at 22:00):

whereas `slim_check.sampleable`

is for types

#### Yury G. Kudryashov (Mar 22 2021 at 22:05):

Adam Topaz said:

But it's true if you replace intersection with union

I should've been more careful. I prove the statement that is correct but didn't fix the type.

#### Patrick Massot (Mar 22 2021 at 22:11):

Legendary post: what happens when Yury answers Zulip questions by typing Lean code away from Lean? He types the proof of the intended statement without reading the actual statement... Now we know how he needs Lean.

#### Jeremy Avigad (Mar 22 2021 at 22:22):

What I am curious to know is how he typed the unicode characters in Zulip without cutting and pasting from Lean.

#### Mario Carneiro (Mar 22 2021 at 23:07):

I often assemble code snippets from the OP's code

#### Jeremy Avigad (Mar 22 2021 at 23:23):

I thought of that, but at least he had to scrounge for the angle brackets. So I wondered whether there is some nifty trick.

#### Julian Berman (Mar 22 2021 at 23:25):

on android those angle brackets are on the long-press keyboard for < (at least in gboard)

#### Yury G. Kudryashov (Mar 22 2021 at 23:44):

@Jeremy Avigad XCompose

Last updated: May 11 2021 at 17:39 UTC