Mathlib.Data.Fintype.Option

instFintypeOption instance

{α : Type*} [Fintype α] : Fintype (Option α)

Full source

instance {α : Type*} [Fintype α] : Fintype (Option α) :=
  ⟨Finset.insertNone univ, fun a => by simp⟩

Finite Option Type

Informal description

For any finite type $\alpha$, the type $\text{Option }\alpha$ (consisting of $\alpha$ plus an additional element $\text{none}$) is also finite.

univ_option theorem

(α : Type*) [Fintype α] : (univ : Finset (Option α)) = insertNone univ

Full source

theorem univ_option (α : Type*) [Fintype α] : (univ : Finset (Option α)) = insertNone univ :=
  rfl

Universal finite set of option type equals insertion of none into universal finite set

Informal description

For any finite type $\alpha$, the universal finite set of the option type $\operatorname{Option} \alpha$ is equal to the insertion of the element $\operatorname{none}$ into the universal finite set of $\alpha$.

Fintype.card_option theorem

{α : Type*} [Fintype α] : Fintype.card (Option α) = Fintype.card α + 1

Full source

@[simp]
theorem Fintype.card_option {α : Type*} [Fintype α] :
    Fintype.card (Option α) = Fintype.card α + 1 :=
  (Finset.card_cons (by simp)).trans <| congr_arg₂ _ (card_map _) rfl

Cardinality of Option Type: $|\operatorname{Option} \alpha| = |\alpha| + 1$

Informal description

For any finite type $\alpha$, the cardinality of the type $\operatorname{Option} \alpha$ (which consists of $\alpha$ plus an additional element $\operatorname{none}$) is equal to the cardinality of $\alpha$ plus one, i.e., $|\operatorname{Option} \alpha| = |\alpha| + 1$.

fintypeOfOption definition

{α : Type*} [Fintype (Option α)] : Fintype α

Full source

/-- If `Option α` is a `Fintype` then so is `α` -/
def fintypeOfOption {α : Type*} [Fintype (Option α)] : Fintype α :=
  ⟨Finset.eraseNone (Fintype.elems (α := Option α)), fun x =>
    mem_eraseNone.mpr (Fintype.complete (some x))⟩

Finite type from finite option type

Informal description

Given a type $\alpha$, if the type `Option α` (i.e., $\alpha$ with an added `none` element) is finite, then $\alpha$ itself is finite. This is constructed by removing the `none` element from the finite set of `Option α` and using the remaining elements as the finite set for $\alpha$.

fintypeOfOptionEquiv definition

[Fintype α] (f : α ≃ Option β) : Fintype β

Full source

/-- A type is a `Fintype` if its successor (using `Option`) is a `Fintype`. -/
def fintypeOfOptionEquiv [Fintype α] (f : α ≃ Option β) : Fintype β :=
  haveI := Fintype.ofEquiv _ f
  fintypeOfOption

Finite type via equivalence with option type

Informal description

Given a finite type $\alpha$ and a type equivalence (bijection) $f : \alpha \simeq \operatorname{Option} \beta$, the type $\beta$ is also finite. This is constructed by first showing that $\operatorname{Option} \beta$ is finite via the equivalence $f$, and then using the fact that $\beta$ is finite when $\operatorname{Option} \beta$ is finite.

Fintype.truncRecEmptyOption definition

 {P : Type u → Sort v} (of_equiv : ∀ {α β}, α ≃ β → P α → P β) (h_empty : P PEmpty)
  (h_option : ∀ {α} [Fintype α] [DecidableEq α], P α → P (Option α)) (α : Type u) [Fintype α] [DecidableEq α] :
  Trunc (P α)

Full source

/-- A recursor principle for finite types, analogous to `Nat.rec`. It effectively says
that every `Fintype` is either `Empty` or `Option α`, up to an `Equiv`. -/
def truncRecEmptyOption {P : Type u → Sort v} (of_equiv : ∀ {α β}, α ≃ β → P α → P β)
    (h_empty : P PEmpty) (h_option : ∀ {α} [Fintype α] [DecidableEq α], P α → P (Option α))
    (α : Type u) [Fintype α] [DecidableEq α] : Trunc (P α) := by
  suffices ∀ n : ℕ, Trunc (P (ULift <| Fin n)) by
    apply Trunc.bind (this (Fintype.card α))
    intro h
    apply Trunc.map _ (Fintype.truncEquivFin α)
    intro e
    exact of_equiv (Equiv.ulift.trans e.symm) h
  intro n
  induction n with
  | zero =>
    have : card PEmpty = card (ULift (Fin 0)) := by
      simp only [card_fin, card_pempty, card_ulift]
    apply Trunc.bind (truncEquivOfCardEq this)
    intro e
    apply Trunc.mk
    exact of_equiv e h_empty
  | succ n ih =>
    have : card (Option (ULift (Fin n))) = card (ULift (Fin n.succ)) := by
      simp only [card_fin, card_option, card_ulift]
    apply Trunc.bind (truncEquivOfCardEq this)
    intro e
    apply Trunc.map _ ih
    intro ih
    exact of_equiv e (h_option ih)

Recursor for finite types via empty and option cases

Informal description

Given a type family `P : Type u → Sort v` and functions: - `of_equiv` that transports `P` along type equivalences, - `h_empty` providing an instance of `P PEmpty`, and - `h_option` extending `P α` to `P (Option α)` for any finite type `α` with decidable equality, then for any finite type `α` with decidable equality, there exists a truncation of `P α`. This is constructed by induction on the cardinality of `α`, using equivalences with `Fin n` and `Option` types.

Fintype.induction_empty_option theorem

 {P : ∀ (α : Type u) [Fintype α], Prop}
  (of_equiv : ∀ (α β) [Fintype β] (e : α ≃ β), @P α (@Fintype.ofEquiv α β ‹_› e.symm) → @P β ‹_›) (h_empty : P PEmpty)
  (h_option : ∀ (α) [Fintype α], P α → P (Option α)) (α : Type u) [h_fintype : Fintype α] : P α

Full source

/-- An induction principle for finite types, analogous to `Nat.rec`. It effectively says
that every `Fintype` is either `Empty` or `Option α`, up to an `Equiv`. -/
@[elab_as_elim]
theorem induction_empty_option {P : ∀ (α : Type u) [Fintype α], Prop}
    (of_equiv : ∀ (α β) [Fintype β] (e : α ≃ β), @P α (@Fintype.ofEquiv α β ‹_› e.symm) → @P β ‹_›)
    (h_empty : P PEmpty) (h_option : ∀ (α) [Fintype α], P α → P (Option α)) (α : Type u)
    [h_fintype : Fintype α] : P α := by
  obtain ⟨p⟩ :=
    let f_empty := fun i => by convert h_empty
    let h_option : ∀ {α : Type u} [Fintype α] [DecidableEq α],
          (∀ (h : Fintype α), P α) → ∀ (h : Fintype (Option α)), P (Option α)  := by
      rintro α hα - Pα hα'
      convert h_option α (Pα _)
    @truncRecEmptyOption (fun α => ∀ h, @P α h) (@fun α β e hα hβ => @of_equiv α β hβ e (hα _))
      f_empty h_option α _ (Classical.decEq α)
  exact p _

Induction Principle for Finite Types via Empty and Option Cases

Informal description

Let $P$ be a predicate on finite types. Suppose that: 1. $P$ is preserved under type equivalences, i.e., for any equivalence $e : \alpha \simeq \beta$ between finite types, $P(\alpha)$ implies $P(\beta)$. 2. $P$ holds for the empty type $\text{PEmpty}$. 3. For any finite type $\alpha$, $P(\alpha)$ implies $P(\text{Option }\alpha)$. Then $P(\alpha)$ holds for any finite type $\alpha$.

Finite.induction_empty_option theorem

 {P : Type u → Prop} (of_equiv : ∀ {α β}, α ≃ β → P α → P β) (h_empty : P PEmpty)
  (h_option : ∀ {α} [Fintype α], P α → P (Option α)) (α : Type u) [Finite α] : P α

Full source

/-- An induction principle for finite types, analogous to `Nat.rec`. It effectively says
that every `Fintype` is either `Empty` or `Option α`, up to an `Equiv`. -/
theorem Finite.induction_empty_option {P : Type u → Prop} (of_equiv : ∀ {α β}, α ≃ β → P α → P β)
    (h_empty : P PEmpty) (h_option : ∀ {α} [Fintype α], P α → P (Option α)) (α : Type u)
    [Finite α] : P α := by
  cases nonempty_fintype α
  refine Fintype.induction_empty_option ?_ ?_ ?_ α
  exacts [fun α β _ => of_equiv, h_empty, @h_option]

Induction Principle for Finite Types via Empty and Option Cases

Informal description

Let $P$ be a predicate on types. Suppose that: 1. $P$ is preserved under type equivalences, i.e., for any equivalence $e : \alpha \simeq \beta$, $P(\alpha)$ implies $P(\beta)$. 2. $P$ holds for the empty type $\mathrm{PEmpty}$. 3. For any finite type $\alpha$, $P(\alpha)$ implies $P(\mathrm{Option}\ \alpha)$. Then $P(\alpha)$ holds for any finite type $\alpha$.