Zulip Chat Archive

Stream: maths

Topic: Index of intersection


view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Mar 22 2021 at 21:48):

But it's true if you replace intersection with union

view this post on Zulip 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

view this post on Zulip Ashvni Narayanan (Mar 22 2021 at 21:53):

Yes, that makes sense, thank you!

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Mar 22 2021 at 21:54):

It could tried a couple of finite types.

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Adam Topaz (Mar 22 2021 at 22:00):

Oh, the slim_check.testable class is only for props

view this post on Zulip Adam Topaz (Mar 22 2021 at 22:00):

whereas slim_check.sampleable is for types

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Mar 22 2021 at 23:07):

I often assemble code snippets from the OP's code

view this post on Zulip 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.

view this post on Zulip Julian Berman (Mar 22 2021 at 23:25):

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

view this post on Zulip Yury G. Kudryashov (Mar 22 2021 at 23:44):

@Jeremy Avigad XCompose


Last updated: May 11 2021 at 17:39 UTC