How to proof things about cardinality of finite sets?

Stream: new members

[Philipp SL Schäfer]

Example: Let X be some finite set with cardinality n, let a be some object that is not in X, then how could one proof (in Lean) that the cardinality of X U {a} is n + 1?

I already saw the documentation here: https://leanprover-community.github.io/mathlib4_docs/Mathlib/SetTheory/Cardinal/Finite.html, but I am not sure how to use this exactly.

[Riccardo Brasca]

We have several notions of cardinality in mathlib, but this result should be already there for all of them. Can you state precisely the result you want?

[Riccardo Brasca]

Anyway look for results about card and insert

[Riccardo Brasca]

for example docs#Finset.card_insert_of_not_mem

[David Renshaw]

or maybe docs#Set.ncard_union_eq if you are working in Set rather than Finset

[Kevin Buzzard]

You'll get a better answer if you write a #mwe . Right now there are many ways to translate your question into lean.

[Philipp SL Schäfer]

Thanks everyone! https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Card.html#Noncomputable-Set-Cardinality seems perfect for my use cases. But I just ran into some error I don't understand.

import Mathlib.Tactic
import Mathlib.Data.Set.Card

variable {α : Type u_1} (S : Set α)

example (hfin: Set.Finite S) : S = ∅ → S.encard = 0 := by
  have hempty: {i : ℕ | i < 0} = ∅ := by
    ext x
    rewrite [Set.mem_setOf]
    apply Iff.intro
    intro h; apply Nat.not_succ_le_zero at h
    apply False.elim; exact h
    intro h; apply Set.eq_empty_iff_forall_not_mem.mp at h
    apply False.elim; exact h
    rfl
  have hcard : Set.encard {i : ℕ | i < 0} = 0 := Set.Nat.encard_range 0
  rewrite [hempty] at hcard
  intro h
  rewrite [h]
  exact hcard

Although the hypothesis is exactly the goal as fas as I can tell, i.e.

hcard: Set.encard ∅ = 0
⊢ Set.encard ∅ = 0

using exact hcard does not work. Why is that the case?

The error message is not very helpful:

type mismatch
  hcard
has type
  Set.encard ∅ = 0 : Prop
but is expected to have type
  Set.encard ∅ = 0 : Prop

Since as far as I can tell there is not type mismatch...

[Kevin Buzzard]

One of your empty sets is the empty subset of alpha, the other is the empty subset of Nat. I noticed this by writing convert hcard (which means "try exact and leave the things which weren't exactly the same as new goals") and then hovering over the terms in the new goal in the infoview.

[Kevin Buzzard]

Just to be clear -- if you've been brought up with set theory then you might think that there's only one empty set. But in Lean every type has an empty subset, and the empty subset of X has got type Set X, so it doesn't even make sense to ask whether two empty subsets of two different types are equal, because equality is only defined for two terms of the same type.

[Philipp SL Schäfer]

Okay, I get it! Thanks for taking the time to answer this :)