Index of intersection

Stream: maths

[Ashvni Narayanan]

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]

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]

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]

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

[Adam Topaz]

But it's true if you replace intersection with union

[Kevin Buzzard]

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]

Yes, that makes sense, thank you!

[Adam Topaz]

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]

It could tried a couple of finite types.

[Adam Topaz]

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]

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]

Oh, the slim_check.testable class is only for props

[Adam Topaz]

whereas slim_check.sampleable is for types

[Yury G. Kudryashov]

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]

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]

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

[Mario Carneiro]

I often assemble code snippets from the OP's code

[Jeremy Avigad]

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]

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

[Yury G. Kudryashov]

@Jeremy Avigad XCompose