Need help on proving {1,2,3} and P{1,2,3} are nontrivial

Stream: new members

[Lars Ericson]

Proving that fin 3 is nontrivial works out of the box:

import data.finset.basic
example : nontrivial (fin 3) := fin.nontrivial

However, taking the powerset doesn't work: 𝒫 (fin 3)

So I need to change representations to

def X : set ℕ := ({1, 2, 3} : finset ℕ)

But then I'm not sure of a couple of things:

• How do I construct emptyset and top
• How do I use those constructed objects in a proof

I am stuck on that and sorry here:

import data.finset.basic
def X : set ℕ := ({1, 2, 3} : finset ℕ)
lemma is_nontrivial_X : ∃ (x y : X), x ≠ y := sorry

I have looked at library_search! which has no suggestions and output of suggest and hint which put out some ideas but haven't worked for me so far.

I'm also stuck for powerset. Here I've got 3 ideas and I don't know how to make them work:

import data.finset.basic
def X : set ℕ := ({1, 2, 3} : finset ℕ)
lemma empty_in_PX : (∅ ∈ (𝒫 X)) := sorry
lemma top_in_PX : (⊤ ∈ (𝒫 X)) := sorry
lemma is_nontrivial_PX : ∃ (x y : 𝒫 X), x ≠ y := sorry
instance : nontrivial (𝒫 X) := { exists_pair_ne := is_nontrivial_PX }

Any help greatly appreciated.

[Yakov Pechersky]

Why do you need that powerset?

[Yakov Pechersky]

The number of unique terms of "set (fin 3)" is the cardinality of that powerset

[Alex J. Best]

Nontrivial takes a type as input, not a set so it inserts a coercion which you may not want.
If all the elements you ever want to consider are 1,2,3 I'd recommend starting with fin 3 rather than making subsets of sets, you can just work with set (fin 3) more naturally in lean

def X : set ℕ := ({1, 2, 3} : finset ℕ)

lemma empty_mem_powerset : ∅ ∈ 𝒫 X := by simp
lemma top_in_PX : (⊤ ∈ (𝒫 X)) := sorry -- this is false ⊤ is the set of all naturals which is not a subset of X
lemma is_nontrivial_PX : ∃ (x ∈ 𝒫 X) (y ∈  𝒫 X), x ≠ y := ⟨ {1}, by simp [X], ∅, empty_mem_powerset, begin intros h, exact set.eq_empty_iff_forall_not_mem.mp h 1 rfl, end ⟩
instance : nontrivial (𝒫 X) := { exists_pair_ne := begin simp,rcases is_nontrivial_PX with ⟨x , hx, y, hy, h⟩, use [x, hx, y, hy],  end }

[Lars Ericson]

Thanks I will try set X . I got it in my head I needed 𝒫 X but that's incorrect.

[Lars Ericson]

DONE (most of the work done by library_search!)

import data.finset.basic
def X := fin 3

instance : nontrivial X := fin.nontrivial

instance : nontrivial (set X) :=
begin
  refine nontrivial_of_ne _ _ _,
  exact set.univ,
  exact ∅ ,
  exact set.empty_ne_univ.symm,
end

[Eric Wieser]

Does unfold X, apply_instance work for the second?

[Lars Ericson]

Yes

import data.finset.basic
def X := fin 3

instance : nontrivial (set X) :=
begin
  unfold X,
  apply_instance
end

[Damiano Testa]

Lars Ericson said:

DONE (most of the work done by library_search!)

import data.finset.basic
def X := fin 3

instance : nontrivial X := fin.nontrivial

instance : nontrivial (set X) :=
begin
  refine nontrivial_of_ne _ _ _,
  exact set.univ,
  exact ∅ ,
  exact set.empty_ne_univ.symm,
end

As far as I understand, the three exact after the refine fill in the underscores. Thus, also refine nontrivial_of_ne set.univ ∅ set.empty_ne_univ.symm, finishes the goal. At this point, you can notice that the last underscore is filled in with a proof that ∅ ≠ set.univ, so just this is enough for Lean to figure out what the two sets in question were. Hence, refine nontrivial_of_ne _ _ set.empty_ne_univ.symm,is sufficient information to create a proof. Once you are here, you no longer need tactic mode:

instance : nontrivial (set X) := nontrivial_of_ne _ _ set.empty_ne_univ.symm