Cardinality of s: Set (Fin n)

Stream: new members

[Ilmārs Cīrulis]

Let's have s: Set (Fin n). If I want to define and prove theorem that it's cardinality is less or equal to n, the only way is to use Set.encard, right?

[Ilmārs Cīrulis]

I'm trying to prove

import Mathlib

theorem t {n} (s: Set (Fin n)): s.encard ≤ n := by
  sorry

[Ilmārs Cīrulis]

It seems I did it.

import Mathlib

theorem t {n} (s: Set (Fin n)): s.encard ≤ n := by
  have H: Finite (Fin n) := Finite.of_fintype (Fin n)
  have H0: (@Set.univ (Fin n)).encard = n := by
    simp [Set.encard_univ]
  simp [<- H0, Set.encard_le_encard]

[Eric Paul]

The following also works

import Mathlib

theorem t {n} (s: Set (Fin n)): s.encard ≤ n := by
  simp [Set.Finite.encard_eq_coe_toFinset_card (s := s) (by toFinite_tac),
    card_finset_fin_le]

You can also use ncard

import Mathlib

theorem t {n} (s: Set (Fin n)): s.ncard ≤ n := by
  simp [Set.ncard_eq_toFinset_card s, card_finset_fin_le]

[Ilmārs Cīrulis]

What's the best (computable) way to count the number of fins in the set, if the membership is decidable?

import Mathlib

def count {n} (s: Set (Fin n)) [∀ x, Decidable (x ∈ s)]: ℕ := sorry

[Aaron Liu]

Maybe s.toFinset.card?

[Ilmārs Cīrulis]

Yes, that works. Big thank you!