sUnion of empties

Stream: new members

[Sebastián Galkin]

I don't think I fully grok how sets work. How does one prove the following?

variables (α : Type) (s : set (set α))

example (h: ∀ t, t ∈ s → t = ∅) : ⋃₀ s = ∅ := sorry

[Scott Morrison]

There are many many proofs. The first thing I hit was

variables (α : Type) (s : set (set α))

example (h: ∀ t, t ∈ s → t = ∅) : ⋃₀ s = ∅ :=
begin
  ext x, simp, intros t m, rw h _ m, simp,
end

[Scott Morrison]

The thinking goes

• "we're trying to prove sets are equal, so lets do it elementwise" : ext
• "presumably mathlib knows something about this situation": simp
• "we're trying to prove something with universal quantifiers: intros
• "the hypothesis h looks helpful, and we now have a suitable argument for it:" rw
• "surely it's easy from here": simp

[Scott Morrison]

I don't doubt that one of our golfers will come up with something shorter. :-)

[Scott Morrison]

And I'm sure a pure term mode proof is available too.

[Scott Morrison]

If you try by suggest

[Scott Morrison]

the top result is exact Sup_eq_bot.mpr h

[Scott Morrison]

i.e. this lemma is already in the library (unsuprisingly)

[Scott Morrison]

src#Sup_eq_bot

[Scott Morrison]

which is a term mode proof

[Sebastián Galkin]

Learning a ton from your answer, thank you so much!

That first simp makes everything much clearer, that's the big step I was missing.

[Scott Morrison]

ext is an extremely useful tactic, that does many things. But generally it means "prove an equality 'componentwise'".

[Jean Lo]

heh, I tried by suggest, got briefly confused, and then realised it wasn't finding the theorem because I hadn't imported data.set.lattice. so here's a (probably very not-idiomatic) term-mode proof that does not invoke the properties of a complete lattice, and proceeds naïvely by "set α in lean is just α → Prop":

variables (α : Type) (s : set (set α))

example (h: ∀ t, t ∈ s → t = ∅) : ⋃₀ s = ∅ :=
set.ext (λ x, iff.intro
  (λ hx, let ⟨_, ha, hs⟩ := hx in false.elim (show x ∈ (∅ : set α), from h _ ha ▸ hs))
  (λ hx, false.elim hx))

[Sebastián Galkin]

ext is an extremely useful tactic

I got that far, but after ext, I didn't know how to turn the set membership proposition into something I could intro. I guess I still don't understand what x ∈ s means exactly

[Sebastián Galkin]

Even this much simpler thing, I'm not sure how to prove:

example (α : Type*) (a b : α) (s: set α) (h: a ∈ s) (b ∉ s) : a ≠ b := sorry

suggest doesn't seem to help much.

[Sebastián Galkin]

Ok, yeah, that was actually easy

example (α : Type*) (a b : α) (s: set α) (h: a ∈ s) (b ∉ s) : a ≠ b :=
begin
intros eq,
rw eq at h,
contradiction,
end

[Kevin Buzzard]

@Sebastián Galkin Internally a subset of X, ie s : set X, is just implemented as a function s : X -> Prop and x \in s is sugar for s x. But all the interface is there for you to not have to think about this internal representation.