set exponentiation in mathlib

Stream: general

[ZHAO Jinxiang]

Is there any definition standing for set exponentiation in lean's mathlib?

https://en.wikipedia.org/wiki/Function_(mathematics)#Set_exponentiation

[Eric Rodriguez]

X → Y

[ZHAO Jinxiang]

I'm asking this, because I want to prove Y ^ ∅ = { ∅ } and ∅ ^ X = ∅ .

[Eric Wieser]

Or maybe docs#set.pi

[Eric Wieser]

Your second lemma is docs#set.pi_eq_empty, but your first lemma isn't true for that definition

[Eric Rodriguez]

docs#function.is_empty is one way you could state the second one. docs#pi.unique_of_is_empty is also a way to state the second one, although a bit harder to understand why

[Kevin Buzzard]

ZHAO Jinxiang said:

I'm asking this, because I want to prove Y ^ ∅ = { ∅ } and ∅ ^ X = ∅ .

They can't both be true :-)

[Kevin Buzzard]

Lean uses type theory, not set theory: for example, the empty function is not equal to the empty type.

[Patrick Johnson]

What you probably want is docs#Set.funs. You can define set exponentiation as

local infixr ` ^ `:80 := λ a b, Set.funs b a

and you can prove your theorems:

Y ^ ∅ = {∅}

example {Y : Set} : Y ^ ∅ = {∅} :=
begin
  refine Set.ext (λ a, _),
  rw [Set.mem_funs, Set.is_func, Set.mem_singleton],
  split; intro h,
  { rw Set.eq_empty,
    rintro _ h₁,
    have h := h.1 h₁,
    rw Set.mem_prod at h,
    cases Set.mem_empty _ h.some_spec.some },
  { subst h,
    split,
    { rw Set.subset_def,
      rintro _ h,
      cases Set.mem_empty _ h },
    { simp }},
end

∅ ^ X = ∅

example {X : Set} (h : X ≠ ∅) : ∅ ^ X = ∅ :=
begin
  refine Set.ext (λ a, _),
  rw [Set.mem_funs, Set.is_func],
  split; intro h₁,
  { cases h₁ with h₂ h₁,
    replace h₂ : a = ∅,
    { rw Set.eq_empty,
      rintro b h₃,
      specialize h₂ h₃,
      rw Set.mem_prod at h₂,
      rcases h₂ with ⟨_, _, _, h₂, _⟩,
      cases Set.mem_empty _ h₂ },
    subst a,
    change ¬_ at h,
    rw ←Set.ext_iff at h,
    apply h.elim, intro b,
    split; intro h,
    { specialize h₁ _ h,
      rcases h₁ with ⟨_, h₁, _⟩,
      cases Set.mem_empty _ h₁ },
    { cases Set.mem_empty _ h }},
  { cases Set.mem_empty _ h₁ },
end

[Eric Rodriguez]

should you not instead do it by giving Set a has_pow instance? (also, Zhao, note that docs#Set is what you do _solely_ for set theory - for normal mathematics, you'd use a type)

[Patrick Johnson]

Eric Rodriguez said:

should you not instead do it by giving Set a has_pow instance?

Of course, has_pow instance would be better, but I can't make it work for some reason.

instance : has_pow Set Set := ⟨λ a b, Set.funs b a⟩
variables {X Y : Set}
#check X ^ Y -- failed to synthesize type class instance for `has_pow Set Set`

Maybe I made some silly mistake?

[Eric Rodriguez]

it's a universe issue, funs is only defined on the same universe so Lean gets confused unless you specify everything:

import set_theory.zfc

universes u

instance : has_pow Set.{u} Set.{u} := ⟨λ a b, Set.funs b a⟩

variables {X Y : Set.{u}}

#check X ^ Y

[Eric Rodriguez]

(the .{u}s are a bit redundant on the first one, but they're there to show a point)

[Patrick Johnson]

Thinking about it, maybe this is a special case when local notation is better. Defining a has_pow instance would require type annotations for ∅ and {...} whenever Lean can't unambiguously infer the Set type for has_pow and it will make theorem statements uglier. And besides that, ZFC theory is pretty much exclusive regarding the rest of mathlib, so when working in set theory we usually don't need other has_pow instances anyway.

[Violeta Hernández]

Eric Rodriguez said:

should you not instead do it by giving Set a has_pow instance? (also, Zhao, note that docs#Set is what you do _solely_ for set theory - for normal mathematics, you'd use a type)

More specifically, it's what you use solely for ZFC set theory. I don't think it's even used in mathlib outside of the file it's defined in.

[Violeta Hernández]

Yeah haha, set_theory/zfc.lean is a leaf file