Fintype.card_option
theorem Fintype.card_option : ∀ {α : Type u_4} [inst : Fintype α], Fintype.card (Option α) = Fintype.card α + 1 := by
sorry
The theorem `Fintype.card_option` states that for any type `α` (assumed to be a finite type, or `Fintype`), the cardinality of the type `Option α` (that is, the number of distinct elements it can have) is equal to the cardinality of `α` plus one. This makes sense because the `Option α` type includes all the values of `α` plus the additional `None` value.
More concisely: The cardinality of `Option α` is equal to the cardinality of `α` plus one, where `α` is a finite type.
|
Finite.induction_empty_option
theorem Finite.induction_empty_option :
∀ {P : Type u → Prop},
(∀ {α β : Type u}, α ≃ β → P α → P β) →
P PEmpty.{u + 1} →
(∀ {α : Type u} [inst : Fintype α], P α → P (Option α)) → ∀ (α : Type u) [inst : Finite α], P α
This theorem, `Finite.induction_empty_option`, is an induction principle for finite types, similar to the induction principle for natural numbers, `Nat.rec`. It states that for a particular property `P`, if `P` holds for an empty type (`PEmpty`) and if `P` holds for any finite type `α`, it also holds for the type `Option α`, then `P` holds for all finite types `α`. Furthermore, this principle acknowledges the fact that if two types `α` and `β` are equivalent (`α ≃ β`), then if `P` holds for `α` it also holds for `β`.
More concisely: If `P` is a property that holds for the empty type and for any finite type `α` such that `Option α` is also a finite type, and `α ≃ β` implies `P` for all types `α` and `β`, then `P` holds for all finite types `α`.
|
Fintype.induction_empty_option
theorem Fintype.induction_empty_option :
∀ {P : (α : Type u) → [inst : Fintype α] → Prop},
(∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β) →
P PEmpty.{u + 1} →
(∀ (α : Type u) [inst : Fintype α], P α → P (Option α)) → ∀ (α : Type u) [h_fintype : Fintype α], P α
This theorem, `Fintype.induction_empty_option`, is an induction principle for finite types, similar to the `Nat.rec` principle used for natural numbers. It essentially states that for any property `P` that applies to finite types, if `P` holds for an empty type and for any finite type `α`, `P` also holds for `Option α` (which can be seen as adding an extra distinct element to `α`), then `P` must hold for all finite types `α`. The property's validity can be transferred between equivalent finite types (types `α` and `β` that have a bijective function `e : α ≃ β`).
More concisely: If a property holds for the empty type and is closed under adding an extra distinct element ( Option type), and if it is preserved under type equivalence, then it holds for all finite types.
|