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

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)