Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-
Copyright (c) 2017 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
! This file was ported from Lean 3 source module data.fintype.basic
! leanprover-community/mathlib commit d78597269638367c3863d40d45108f52207e03cf
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Finset.Image
/-!
# Finite types
This file defines a typeclass to state that a type is finite.
## Main declarations
* `Fintype α`: Typeclass saying that a type is finite. It takes as fields a `Finset` and a proof
that all terms of type `α` are in it.
* `Finset.univ`: The finset of all elements of a fintype.
See `Data.Fintype.Card` for the cardinality of a fintype,
the equivalence with `Fin (Fintype.card α)`, and pigeonhole principles.
## Instances
Instances for `Fintype` for
* `{x // p x}` are in this file as `Fintype.subtype`
* `Option α` are in `Data.Fintype.Option`
* `α × β` are in `Data.Fintype.Prod`
* `α ⊕ β` are in `Data.Fintype.Sum`
* `Σ (a : α), β a` are in `Data.Fintype.Sigma`
These files also contain appropriate `Infinite` instances for these types.
`Infinite` instances for `ℕ`, `ℤ`, `Multiset α`, and `List α` are in `Data.Fintype.Lattice`.
Types which have a surjection from/an injection to a `Fintype` are themselves fintypes.
See `Fintype.ofInjective` and `Fintype.ofSurjective`.
-/
open Function
open Nat
universe u v
variable { α β γ : Type _ : Type (?u.152214+1)}
/-- `Fintype α` means that `α` is finite, i.e. there are only
finitely many distinct elements of type `α`. The evidence of this
is a finset `elems` (a list up to permutation without duplicates),
together with a proof that everything of type `α` is in the list. -/
class Fintype ( α : Type _ ) where
/-- The `Finset` containing all elements of a `Fintype` -/
elems : Finset α
/-- A proof that `elems` contains every element of the type -/
complete : ∀ {α : Type u_1} [self : Fintype α x : α ), x ∈ Fintype.elems : ∀ x : α , x ∈ elems
#align fintype Fintype
namespace Finset
variable [ Fintype α ] { s t : Finset α }
/-- `univ` is the universal finite set of type `Finset α` implied from
the assumption `Fintype α`. -/
def univ : Finset α :=
@ Fintype.elems α _
#align finset.univ Finset.univ
@[ simp ]
theorem mem_univ : ∀ {α : Type u_1} [inst : Fintype α x : α ), x ∈ univ mem_univ ( x : α ) : x ∈ ( univ : Finset α ) :=
Fintype.complete : ∀ {α : Type ?u.198} [self : Fintype α x : α ), x ∈ Fintype.elems x
#align finset.mem_univ Finset.mem_univ : ∀ {α : Type u_1} [inst : Fintype α x : α ), x ∈ univ
--Porting note: removing @[simp], simp can prove it
theorem mem_univ_val : ∀ (x : α ), x ∈ univ .val mem_univ_val : ∀ x , x ∈ ( univ : Finset α ). 1 :=
mem_univ : ∀ {α : Type ?u.295} [inst : Fintype α x : α ), x ∈ univ
#align finset.mem_univ_val Finset.mem_univ_val : ∀ {α : Type u_1} [inst : Fintype α x : α ), x ∈ univ .val
theorem eq_univ_iff_forall : s = univ ↔ ∀ (x : α ), x ∈ s eq_univ_iff_forall : s = univ ↔ ∀ x , x ∈ s := by s = univ ↔ ∀ (x : α ), x ∈ s simp [ ext_iff : ∀ {α : Type ?u.412} {s₁ s₂ : Finset α s₁ = s₂ ↔ ∀ (a : α ), a ∈ s₁ ↔ a ∈ s₂ ]
#align finset.eq_univ_iff_forall Finset.eq_univ_iff_forall : ∀ {α : Type u_1} [inst : Fintype α s : Finset α s = univ ↔ ∀ (x : α ), x ∈ s
theorem eq_univ_of_forall : (∀ (x : α ), x ∈ s ) → s = univ eq_univ_of_forall : (∀ x , x ∈ s ) → s = univ :=
eq_univ_iff_forall : ∀ {α : Type ?u.1041} [inst : Fintype α s : Finset α s = univ ↔ ∀ (x : α ), x ∈ s . 2 : ∀ {a b : Prop }, (a ↔ b b → a
#align finset.eq_univ_of_forall Finset.eq_univ_of_forall : ∀ {α : Type u_1} [inst : Fintype α s : Finset α (∀ (x : α ), x ∈ s ) → s = univ
@[ simp , norm_cast ]
theorem coe_univ : ↑univ = Set.univ coe_univ : ↑( univ : Finset α ) = ( Set.univ : {α : Type ?u.1102} → Set α : Set α ) := by ext h x✝ ∈ ↑univ ↔ x✝ ∈ Set.univ ; h x✝ ∈ ↑univ ↔ x✝ ∈ Set.univ simp
#align finset.coe_univ Finset.coe_univ : ∀ {α : Type u_1} [inst : Fintype α ↑univ = Set.univ
@[ simp , norm_cast ]
theorem coe_eq_univ : ↑s = Set.univ ↔ s = univ coe_eq_univ : ( s : Set α ) = Set.univ : {α : Type ?u.1498} → Set α ↔ s = univ := by rw [ ← coe_univ : ∀ {α : Type ?u.1568} [inst : Fintype α ↑univ = Set.univ , coe_inj : ∀ {α : Type ?u.1581} {s₁ s₂ : Finset α ↑s₁ = ↑s₂ ↔ s₁ = s₂ ]
#align finset.coe_eq_univ Finset.coe_eq_univ
theorem Nonempty.eq_univ [ Subsingleton α ] : s . Nonempty → s = univ := by
rintro ⟨ x , hx ⟩
refine' eq_univ_of_forall : ∀ {α : Type ?u.1809} [inst : Fintype α s : Finset α (∀ (x : α ), x ∈ s ) → s = univ fun y => by rwa [ Subsingleton.elim y x ]
#align finset.nonempty.eq_univ Finset.Nonempty.eq_univ
theorem univ_nonempty_iff : ( univ : Finset α ). Nonempty ↔ Nonempty α := by
rw [ ← coe_nonempty , coe_univ : ∀ {α : Type ?u.1902} [inst : Fintype α ↑univ = Set.univ , Set.nonempty_iff_univ_nonempty ]
#align finset.univ_nonempty_iff Finset.univ_nonempty_iff
theorem univ_nonempty [ Nonempty α ] : ( univ : Finset α ). Nonempty :=
univ_nonempty_iff . 2 : ∀ {a b : Prop }, (a ↔ b b → a ‹_›
#align finset.univ_nonempty Finset.univ_nonempty
theorem univ_eq_empty_iff : ( univ : Finset α ) = ∅ ↔ IsEmpty α := by
rw [ ← not_nonempty_iff , ← univ_nonempty_iff , not_nonempty_iff_eq_empty ]
#align finset.univ_eq_empty_iff Finset.univ_eq_empty_iff
@[ simp ]
theorem univ_eq_empty [ IsEmpty α ] : ( univ : Finset α ) = ∅ :=
univ_eq_empty_iff . 2 : ∀ {a b : Prop }, (a ↔ b b → a ‹_›
#align finset.univ_eq_empty Finset.univ_eq_empty
@[ simp ]
theorem univ_unique : ∀ [inst : Unique α univ = {default } univ_unique [ Unique : Sort ?u.2321 → Sort (max1?u.2321) α ] : ( univ : Finset α ) = { default } :=
Finset.ext : ∀ {α : Type ?u.3348} {s₁ s₂ : Finset α (∀ (a : α ), a ∈ s₁ ↔ a ∈ s₂ ) → s₁ = s₂ fun x => iff_of_true : ∀ {a b : Prop }, a → b → (a ↔ b ( mem_univ : ∀ {α : Type ?u.3363} [inst : Fintype α x : α ), x ∈ univ _ ) <| mem_singleton : ∀ {α : Type ?u.3381} {a b : α }, b ∈ {a } ↔ b = a . 2 : ∀ {a b : Prop }, (a ↔ b b → a <| Subsingleton.elim x default
#align finset.univ_unique Finset.univ_unique : ∀ {α : Type u_1} [inst : Fintype α inst_1 : Unique α univ = {default }
@[ simp ]
theorem subset_univ ( s : Finset α ) : s ⊆ univ := fun a _ => mem_univ : ∀ {α : Type ?u.3641} [inst : Fintype α x : α ), x ∈ univ a
#align finset.subset_univ Finset.subset_univ
instance boundedOrder : BoundedOrder : (α : Type ?u.3690) → [inst : LE α Type ?u.3690 ( Finset α ) :=
{ inferInstanceAs : (α : Sort ?u.3727) → [i : α ] → α ( OrderBot : (α : Type ?u.3728) → [inst : LE α Type ?u.3728 ( Finset α )) with
top := univ
le_top := subset_univ }
#align finset.bounded_order Finset.boundedOrder
@[ simp ]
theorem top_eq_univ : ( ⊤ : Finset α ) = univ :=
rfl : ∀ {α : Sort ?u.4125} {a : α }, a = a
#align finset.top_eq_univ Finset.top_eq_univ : ∀ {α : Type u_1} [inst : Fintype α ⊤ = univ
theorem ssubset_univ_iff { s : Finset α } : s ⊂ univ ↔ s ≠ univ :=
@ lt_top_iff_ne_top _ _ _ s
#align finset.ssubset_univ_iff Finset.ssubset_univ_iff
theorem codisjoint_left : Codisjoint s t ↔ ∀ ⦃ a ⦄, a ∉ s → a ∈ t := by
classical simp [ codisjoint_iff , eq_univ_iff_forall : ∀ {α : Type ?u.4420} [inst : Fintype α s : Finset α s = univ ↔ ∀ (x : α ), x ∈ s , or_iff_not_imp_left : ∀ {a b : Prop }, a ∨ b ↔ ¬ a b ]
#align finset.codisjoint_left Finset.codisjoint_left
theorem codisjoint_right : Codisjoint s t ↔ ∀ ⦃ a ⦄, a ∉ t → a ∈ s :=
Codisjoint_comm . trans : ∀ {a b c : Prop }, (a ↔ b (b ↔ c a ↔ c codisjoint_left
#align finset.codisjoint_right Finset.codisjoint_right
section BooleanAlgebra
variable [ DecidableEq : Sort ?u.9320 → Sort (max1?u.9320) α ] { a : α }
instance booleanAlgebra : BooleanAlgebra : Type ?u.7153 → Type ?u.7153 ( Finset α ) :=
GeneralizedBooleanAlgebra.toBooleanAlgebra
#align finset.boolean_algebra Finset.booleanAlgebra
theorem sdiff_eq_inter_compl : ∀ (s t : Finset α s \ t = s ∩ t ᶜ sdiff_eq_inter_compl ( s t : Finset α ) : s \ t = s ∩ t ᶜ :=
sdiff_eq
#align finset.sdiff_eq_inter_compl Finset.sdiff_eq_inter_compl
theorem compl_eq_univ_sdiff ( s : Finset α ) : s ᶜ = univ \ s :=
rfl : ∀ {α : Sort ?u.7755} {a : α }, a = a
#align finset.compl_eq_univ_sdiff Finset.compl_eq_univ_sdiff
@[ simp ]
theorem mem_compl : a ∈ s ᶜ ↔ a ∉ s := by simp [ compl_eq_univ_sdiff ]
#align finset.mem_compl Finset.mem_compl
theorem not_mem_compl : ¬ a ∈ s ᶜ ↔ a ∈ s not_mem_compl : a ∉ s ᶜ ↔ a ∈ s := by rw [ mem_compl , not_not ]
#align finset.not_mem_compl Finset.not_mem_compl
@[ simp , norm_cast ]
theorem coe_compl ( s : Finset α ) : ↑( s ᶜ) = (↑ s : Set α )ᶜ :=
Set.ext : ∀ {α : Type ?u.8791} {a b : Set α (∀ (x : α ), x ∈ a ↔ x ∈ b ) → a = b fun _ => mem_compl
#align finset.coe_compl Finset.coe_compl
@[ simp ]
theorem compl_empty : ( ∅ : Finset α )ᶜ = univ :=
compl_bot
#align finset.compl_empty Finset.compl_empty
@[ simp ]
theorem compl_univ : ( univ : Finset α )ᶜ = ∅ :=
compl_top
#align finset.compl_univ Finset.compl_univ
@[ simp ]
theorem compl_eq_empty_iff ( s : Finset α ) : s ᶜ = ∅ ↔ s = univ :=
compl_eq_bot
#align finset.compl_eq_empty_iff Finset.compl_eq_empty_iff
@[ simp ]
theorem compl_eq_univ_iff ( s : Finset α ) : s ᶜ = univ ↔ s = ∅ :=
compl_eq_top
#align finset.compl_eq_univ_iff Finset.compl_eq_univ_iff
@[ simp ]
theorem union_compl ( s : Finset α ) : s ∪ s ᶜ = univ :=
sup_compl_eq_top
#align finset.union_compl Finset.union_compl
@[ simp ]
theorem inter_compl ( s : Finset α ) : s ∩ s ᶜ = ∅ :=
inf_compl_eq_bot
#align finset.inter_compl Finset.inter_compl
@[ simp ]
theorem compl_union ( s t : Finset α ) : ( s ∪ t )ᶜ = s ᶜ ∩ t ᶜ :=
compl_sup
#align finset.compl_union Finset.compl_union
@[ simp ]
theorem compl_inter ( s t : Finset α ) : ( s ∩ t )ᶜ = s ᶜ ∪ t ᶜ :=
compl_inf
#align finset.compl_inter Finset.compl_inter
@[ simp ]
theorem compl_erase : s . erase a ᶜ = insert a ( s ᶜ) := by
ext
simp only [ or_iff_not_imp_left : ∀ {a b : Prop }, a ∨ b ↔ ¬ a b , mem_insert , not_and : ∀ {a b : Prop }, ¬ (a ∧ b ↔ a → ¬ b , mem_compl , mem_erase ]
#align finset.compl_erase Finset.compl_erase
@[ simp ]
theorem compl_insert : insert a s ᶜ = s ᶜ. erase a := by
ext
simp only [ not_or , mem_insert , iff_self_iff , mem_compl , mem_erase ]
#align finset.compl_insert Finset.compl_insert
@[ simp ]
theorem insert_compl_self ( x : α ) : insert x ({ x }ᶜ : Finset α ) = univ := by
rw [ ← compl_erase , erase_singleton , compl_empty ]
#align finset.insert_compl_self Finset.insert_compl_self
@[ simp ]
theorem compl_filter ( p : α → Prop ) [ DecidablePred : {α : Sort ?u.13608} → (α → Prop Sort (max1?u.13608) p ] [∀ x , Decidable ¬ p x ] :
univ . filter p ᶜ = univ . filter fun x => ¬ p x :=
ext : ∀ {α : Type ?u.13769} {s₁ s₂ : Finset α (∀ (a : α ), a ∈ s₁ ↔ a ∈ s₂ ) → s₁ = s₂ <| by simp
#align finset.compl_filter Finset.compl_filter
theorem compl_ne_univ_iff_nonempty ( s : Finset α ) : s ᶜ ≠ univ ↔ s . Nonempty := by
simp [ eq_univ_iff_forall : ∀ {α : Type ?u.16684} [inst : Fintype α s : Finset α s = univ ↔ ∀ (x : α ), x ∈ s , Finset.Nonempty ]
#align finset.compl_ne_univ_iff_nonempty Finset.compl_ne_univ_iff_nonempty
theorem compl_singleton : ∀ (a : α ), {a } ᶜ = erase univ a compl_singleton ( a : α ) : ({ a } : Finset α )ᶜ = univ . erase a := by
rw [ compl_eq_univ_sdiff , sdiff_singleton_eq_erase ]
#align finset.compl_singleton Finset.compl_singleton
theorem insert_inj_on' ( s : Finset α ) : Set.InjOn : {α : Type ?u.19171} → {β : Type ?u.19170} → (α → β Set α Prop ( fun a => insert a s ) ( s ᶜ : Finset α ) := by
rw [ coe_compl ]
exact s . insert_inj_on
#align finset.insert_inj_on' Finset.insert_inj_on'
theorem image_univ_of_surjective [ Fintype β ] { f : β → α } ( hf : Surjective : {α : Sort ?u.19639} → {β : Sort ?u.19638} → (α → β Prop f ) :
univ . image f = univ :=
eq_univ_of_forall : ∀ {α : Type ?u.19754} [inst : Fintype α s : Finset α (∀ (x : α ), x ∈ s ) → s = univ <| hf . forall : ∀ {α : Sort ?u.19768} {β : Sort ?u.19769} {f : α → β Surjective f ∀ {p : β → Prop (∀ (y : β ), p y ) ↔ ∀ (x : α ), p (f x . 2 : ∀ {a b : Prop }, (a ↔ b b → a fun _ => mem_image_of_mem _ <| mem_univ : ∀ {α : Type ?u.19878} [inst : Fintype α x : α ), x ∈ univ _
#align finset.image_univ_of_surjective Finset.image_univ_of_surjective
end BooleanAlgebra
theorem map_univ_of_surjective [ Fintype β ] { f : β ↪ α } ( hf : Surjective : {α : Sort ?u.19975} → {β : Sort ?u.19974} → (α → β Prop f ) : univ . map f = univ :=
eq_univ_of_forall : ∀ {α : Type ?u.20913} [inst : Fintype α s : Finset α (∀ (x : α ), x ∈ s ) → s = univ <| hf . forall : ∀ {α : Sort ?u.20927} {β : Sort ?u.20928} {f : α → β Surjective f ∀ {p : β → Prop (∀ (y : β ), p y ) ↔ ∀ (x : α ), p (f x . 2 : ∀ {a b : Prop }, (a ↔ b b → a fun _ => mem_map_of_mem : ∀ {α : Type ?u.20951} {β : Type ?u.20952} (f : α ↪ β a : α } {s : Finset α a ∈ s ↑f a ∈ map f s _ <| mem_univ : ∀ {α : Type ?u.20984} [inst : Fintype α x : α ), x ∈ univ _
#align finset.map_univ_of_surjective Finset.map_univ_of_surjective
@[ simp ]
theorem map_univ_equiv [ Fintype β ] ( f : β ≃ α ) : univ . map f . toEmbedding : {α : Sort ?u.21064} → {β : Sort ?u.21063} → α ≃ β α ↪ β = univ :=
map_univ_of_surjective f . surjective
#align finset.map_univ_equiv Finset.map_univ_equiv
@[ simp ]
theorem univ_inter [ DecidableEq : Sort ?u.21209 → Sort (max1?u.21209) α ] ( s : Finset α ) : univ ∩ s = s :=
ext : ∀ {α : Type ?u.21277} {s₁ s₂ : Finset α (∀ (a : α ), a ∈ s₁ ↔ a ∈ s₂ ) → s₁ = s₂ fun a => by simp
#align finset.univ_inter Finset.univ_inter
@[ simp ]
theorem inter_univ [ DecidableEq : Sort ?u.21506 → Sort (max1?u.21506) α ] ( s : Finset α ) : s ∩ univ = s := by rw [ inter_comm , univ_inter ]
#align finset.inter_univ Finset.inter_univ
@[ simp ]
theorem piecewise_univ [∀ i : α , Decidable ( i ∈ ( univ : Finset α ))] { δ : α → Sort _ }
( f g : ∀ i , δ i ) : univ . piecewise : {α : Type ?u.21962} →
{δ : α → Sort ?u.21961(s : Finset α ((i : α ) → δ i ) → ((i : α ) → δ i ) → [inst : (j : α ) → Decidable (j ∈ s ] → (i : α ) → δ i f g = f := by
ext i
simp [ piecewise : {α : Type ?u.22065} →
{δ : α → Sort ?u.22064(s : Finset α ((i : α ) → δ i ) → ((i : α ) → δ i ) → [inst : (j : α ) → Decidable (j ∈ s ] → (i : α ) → δ i ]
#align finset.piecewise_univ Finset.piecewise_univ
theorem piecewise_compl [ DecidableEq : Sort ?u.22265 → Sort (max1?u.22265) α ] ( s : Finset α ) [∀ i : α , Decidable ( i ∈ s )]
[∀ i : α , Decidable ( i ∈ s ᶜ)] { δ : α → Sort _ } ( f g : ∀ i , δ i ) :
s ᶜ. piecewise : {α : Type ?u.22442} →
{δ : α → Sort ?u.22441(s : Finset α ((i : α ) → δ i ) → ((i : α ) → δ i ) → [inst : (j : α ) → Decidable (j ∈ s ] → (i : α ) → δ i piecewise f g = s . piecewise : {α : Type ?u.22489} →
{δ : α → Sort ?u.22488(s : Finset α ((i : α ) → δ i ) → ((i : α ) → δ i ) → [inst : (j : α ) → Decidable (j ∈ s ] → (i : α ) → δ i g f := by
ext i
simp [ piecewise : {α : Type ?u.22586} →
{δ : α → Sort ?u.22585(s : Finset α ((i : α ) → δ i ) → ((i : α ) → δ i ) → [inst : (j : α ) → Decidable (j ∈ s ] → (i : α ) → δ i ]
#align finset.piecewise_compl Finset.piecewise_compl
@[ simp ]
theorem piecewise_erase_univ { δ : α → Sort _ } [ DecidableEq : Sort ?u.23073 → Sort (max1?u.23073) α ] ( a : α ) ( f g : ∀ a , δ a ) :
( Finset.univ . erase a ). piecewise : {α : Type ?u.23151} →
{δ : α → Sort ?u.23150(s : Finset α ((i : α ) → δ i ) → ((i : α ) → δ i ) → [inst : (j : α ) → Decidable (j ∈ s ] → (i : α ) → δ i piecewise f g = Function.update : {α : Sort ?u.23253} →
{β : α → Sort ?u.23252[inst : DecidableEq α ((a : α ) → β a ) → (a' : α ) → β a' (a : α ) → β a f a ( g a ) := by
rw [ ← compl_singleton , piecewise_compl , piecewise_singleton ]
#align finset.piecewise_erase_univ Finset.piecewise_erase_univ
theorem univ_map_equiv_to_embedding { α β : Type _ : Type (?u.23867+1)} [ Fintype α ] [ Fintype β ] ( e : α ≃ β ) :
univ . map e . toEmbedding : {α : Sort ?u.23895} → {β : Sort ?u.23894} → α ≃ β α ↪ β = univ :=
eq_univ_iff_forall : ∀ {α : Type ?u.23955} [inst : Fintype α s : Finset α s = univ ↔ ∀ (x : α ), x ∈ s . mpr : ∀ {a b : Prop }, (a ↔ b b → a fun b => mem_map : ∀ {α : Type ?u.23978} {β : Type ?u.23977} {f : α ↪ β s : Finset α b : β }, b ∈ map f s ↔ ∃ a , a ∈ s ∧ ↑f a = b . mpr : ∀ {a b : Prop }, (a ↔ b b → a ⟨ e . symm : {α : Sort ?u.24012} → {β : Sort ?u.24011} → α ≃ β β ≃ α b , mem_univ : ∀ {α : Type ?u.24105} [inst : Fintype α x : α ), x ∈ univ _ , by simp ⟩
#align finset.univ_map_equiv_to_embedding Finset.univ_map_equiv_to_embedding
@[ simp ]
theorem univ_filter_exists ( f : α → β ) [ Fintype β ] [ DecidablePred : {α : Sort ?u.24334} → (α → Prop Sort (max1?u.24334) fun y => ∃ x , f x = y ]
[ DecidableEq : Sort ?u.24355 → Sort (max1?u.24355) β ] : ( Finset.univ . filter fun y => ∃ x , f x = y ) = Finset.univ . image f := by
ext
simp
#align finset.univ_filter_exists Finset.univ_filter_exists
/-- Note this is a special case of `(Finset.image_preimage f univ _).symm`. -/
theorem univ_filter_mem_range ( f : α → β ) [ Fintype β ] [ DecidablePred : {α : Sort ?u.29346} → (α → Prop Sort (max1?u.29346) fun y => y ∈ Set.range : {α : Type ?u.29357} → {ι : Sort ?u.29356} → (ι → α Set α f ]
[ DecidableEq : Sort ?u.29384 → Sort (max1?u.29384) β ] : ( Finset.univ . filter fun y => y ∈ Set.range : {α : Type ?u.29415} → {ι : Sort ?u.29414} → (ι → α Set α f ) = Finset.univ . image f := by
letI : DecidablePred : {α : Sort ?u.29539} → (α → Prop Sort (max1?u.29539) ( fun y => ∃ x , f x = y ) := by simpa using ‹_›
exact univ_filter_exists f
#align finset.univ_filter_mem_range Finset.univ_filter_mem_range
theorem coe_filter_univ ( p : α → Prop ) [ DecidablePred : {α : Sort ?u.31048} → (α → Prop Sort (max1?u.31048) p ] : ( univ . filter p : Set α ) = { x | p x } :=
by simp
#align finset.coe_filter_univ Finset.coe_filter_univ
end Finset
open Finset Function
namespace Fintype
instance decidablePiFintype { α } { β : α → Type _ : Type (?u.31892+1)} [∀ a , DecidableEq : Sort ?u.31899 → Sort (max1?u.31899) ( β a )] [ Fintype α ] :
DecidableEq : Sort ?u.31914 → Sort (max1?u.31914) (∀ a , β a ) := fun f g =>
decidable_of_iff (∀ a ∈ @ Fintype.elems α _, f a = g a )
( by (∀ (a : α ), a ∈ elems f a = g a ) ↔ f = g simp [ Function.funext_iff : ∀ {α : Sort ?u.32076} {β : α → Sort ?u.32075f₁ f₂ : (x : α ) → β x }, f₁ = f₂ ↔ ∀ (a : α ), f₁ a = f₂ a , Fintype.complete : ∀ {α : Type ?u.32098} [self : Fintype α x : α ), x ∈ elems ] )
#align fintype.decidable_pi_fintype Fintype.decidablePiFintype
instance decidableForallFintype { p : α → Prop } [ DecidablePred : {α : Sort ?u.34258} → (α → Prop Sort (max1?u.34258) p ] [ Fintype α ] :
Decidable (∀ a , p a ) :=
decidable_of_iff (∀ a ∈ @ univ α _, p a ) ( by (∀ (a : α ), a ∈ univ p a ) ↔ ∀ (a : α ), p a simp )
#align fintype.decidable_forall_fintype Fintype.decidableForallFintype
instance decidableExistsFintype { p : α → Prop } [ DecidablePred : {α : Sort ?u.35069} → (α → Prop Sort (max1?u.35069) p ] [ Fintype α ] :
Decidable (∃ a , p a ) :=
decidable_of_iff (∃ a ∈ @ univ α _, p a ) ( by (∃ a , a ∈ univ ∧ p a ) ↔ ∃ a , p a simp )
#align fintype.decidable_exists_fintype Fintype.decidableExistsFintype
instance decidableMemRangeFintype [ Fintype α ] [ DecidableEq : Sort ?u.35429 → Sort (max1?u.35429) β ] ( f : α → β ) :
DecidablePred : {α : Sort ?u.35442} → (α → Prop Sort (max1?u.35442) (· ∈ Set.range : {α : Type ?u.35453} → {ι : Sort ?u.35452} → (ι → α Set α f ) := fun _ => Fintype.decidableExistsFintype
#align fintype.decidable_mem_range_fintype Fintype.decidableMemRangeFintype
section BundledHoms
instance decidableEqEquivFintype [ DecidableEq : Sort ?u.35827 → Sort (max1?u.35827) β ] [ Fintype α ] : DecidableEq : Sort ?u.35839 → Sort (max1?u.35839) ( α ≃ β ) := fun a b =>
decidable_of_iff ( a . 1 : {α : Sort ?u.35863} → {β : Sort ?u.35862} → α ≃ β α → β = b . 1 : {α : Sort ?u.35870} → {β : Sort ?u.35869} → α ≃ β α → β ) Equiv.coe_fn_injective : ∀ {α : Sort ?u.35878} {β : Sort ?u.35877}, Injective fun e => ↑e . eq_iff : ∀ {α : Sort ?u.35881} {β : Sort ?u.35882} {f : α → β Injective f ∀ {a b : α }, f a = f b ↔ a = b
#align fintype.decidable_eq_equiv_fintype Fintype.decidableEqEquivFintype
instance decidableEqEmbeddingFintype [ DecidableEq : Sort ?u.36154 → Sort (max1?u.36154) β ] [ Fintype α ] : DecidableEq : Sort ?u.36166 → Sort (max1?u.36166) ( α ↪ β ) := fun a b =>
decidable_of_iff (( a : α → β ) = b ) Function.Embedding.coe_injective : ∀ {α : Sort ?u.38949} {β : Sort ?u.38950}, Injective fun f => ↑f . eq_iff : ∀ {α : Sort ?u.38953} {β : Sort ?u.38954} {f : α → β Injective f ∀ {a b : α }, f a = f b ↔ a = b
#align fintype.decidable_eq_embedding_fintype Fintype.decidableEqEmbeddingFintype
@[ to_additive ]
instance decidableEqOneHomFintype [ DecidableEq : Sort ?u.39302 → Sort (max1?u.39302) β ] [ Fintype α ] [ One α ] [ One β ] :
DecidableEq : Sort ?u.39320 → Sort (max1?u.39320) ( OneHom : (M : Type ?u.39322) → (N : Type ?u.39321) → [inst : One M [inst : One N Type (max?u.39322?u.39321) α β ) := fun a b =>
decidable_of_iff (( a : α → β ) = b ) ( Injective.eq_iff : ∀ {α : Sort ?u.41133} {β : Sort ?u.41134} {f : α → β Injective f ∀ {a b : α }, f a = f b ↔ a = b FunLike.coe_injective )
#align fintype.decidable_eq_one_hom_fintype Fintype.decidableEqOneHomFintype
#align fintype.decidable_eq_zero_hom_fintype Fintype.decidableEqZeroHomFintype
@[ to_additive ]
instance decidableEqMulHomFintype [ DecidableEq : Sort ?u.42242 → Sort (max1?u.42242) β ] [ Fintype α ] [ Mul α ] [ Mul β ] :
DecidableEq : Sort ?u.42260 → Sort (max1?u.42260) ( α →ₙ* β ) := fun a b =>
decidable_of_iff (( a : α → β ) = b ) ( Injective.eq_iff : ∀ {α : Sort ?u.42920} {β : Sort ?u.42921} {f : α → β Injective f ∀ {a b : α }, f a = f b ↔ a = b FunLike.coe_injective )
#align fintype.decidable_eq_mul_hom_fintype Fintype.decidableEqMulHomFintype
#align fintype.decidable_eq_add_hom_fintype Fintype.decidableEqAddHomFintype
@[ to_additive ]
instance decidableEqMonoidHomFintype [ DecidableEq : Sort ?u.43689 → Sort (max1?u.43689) β ] [ Fintype α ] [ MulOneClass : Type ?u.43701 → Type ?u.43701 α ] [ MulOneClass : Type ?u.43704 → Type ?u.43704 β ] :
DecidableEq : Sort ?u.43707 → Sort (max1?u.43707) ( α →* β ) := fun a b =>
decidable_of_iff (( a : α → β ) = b ) ( Injective.eq_iff : ∀ {α : Sort ?u.45037} {β : Sort ?u.45038} {f : α → β Injective f ∀ {a b : α }, f a = f b ↔ a = b FunLike.coe_injective )
#align fintype.decidable_eq_monoid_hom_fintype Fintype.decidableEqMonoidHomFintype
#align fintype.decidable_eq_add_monoid_hom_fintype Fintype.decidableEqAddMonoidHomFintype
instance decidableEqMonoidWithZeroHomFintype [ DecidableEq : Sort ?u.46006 → Sort (max1?u.46006) β ] [ Fintype α ] [ MulZeroOneClass : Type ?u.46018 → Type ?u.46018 α ]
[ MulZeroOneClass : Type ?u.46021 → Type ?u.46021 β ] : DecidableEq : Sort ?u.46024 → Sort (max1?u.46024) ( α →*₀ β ) := fun a b =>
decidable_of_iff (( a : α → β ) = b ) ( Injective.eq_iff : ∀ {α : Sort ?u.47602} {β : Sort ?u.47603} {f : α → β Injective f ∀ {a b : α }, f a = f b ↔ a = b FunLike.coe_injective )
#align fintype.decidable_eq_monoid_with_zero_hom_fintype Fintype.decidableEqMonoidWithZeroHomFintype
instance decidableEqRingHomFintype [ DecidableEq : Sort ?u.48385 → Sort (max1?u.48385) β ] [ Fintype α ] [ Semiring α ] [ Semiring β ] :
DecidableEq : Sort ?u.48403 → Sort (max1?u.48403) ( α →+* β ) := fun a b =>
decidable_of_iff (( a : α → β ) = b ) ( Injective.eq_iff : ∀ {α : Sort ?u.49602} {β : Sort ?u.49603} {f : α → β Injective f ∀ {a b : α }, f a = f b ↔ a = b RingHom.coe_inj )
#align fintype.decidable_eq_ring_hom_fintype Fintype.decidableEqRingHomFintype
end BundledHoms
instance decidableInjectiveFintype [ DecidableEq : Sort ?u.49980 → Sort (max1?u.49980) α ] [ DecidableEq : Sort ?u.49989 → Sort (max1?u.49989) β ] [ Fintype α ] :
DecidablePred : {α : Sort ?u.50001} → (α → Prop Sort (max1?u.50001) ( Injective : {α : Sort ?u.50009} → {β : Sort ?u.50008} → (α → β Prop : ( α → β ) → Prop ) := fun x => by unfold Injective ; infer_instance
#align fintype.decidable_injective_fintype Fintype.decidableInjectiveFintype
instance decidableSurjectiveFintype [ DecidableEq : Sort ?u.50662 → Sort (max1?u.50662) β ] [ Fintype α ] [ Fintype β ] :
DecidablePred : {α : Sort ?u.50677} → (α → Prop Sort (max1?u.50677) ( Surjective : {α : Sort ?u.50685} → {β : Sort ?u.50684} → (α → β Prop : ( α → β ) → Prop ) := fun x => by unfold Surjective ; infer_instance
#align fintype.decidable_surjective_fintype Fintype.decidableSurjectiveFintype
instance decidableBijectiveFintype [ DecidableEq : Sort ?u.51084 → Sort (max1?u.51084) α ] [ DecidableEq : Sort ?u.51093 → Sort (max1?u.51093) β ] [ Fintype α ] [ Fintype β ] :
DecidablePred : {α : Sort ?u.51108} → (α → Prop Sort (max1?u.51108) ( Bijective : {α : Sort ?u.51116} → {β : Sort ?u.51115} → (α → β Prop : ( α → β ) → Prop ) := fun x => by unfold Bijective ; infer_instance
#align fintype.decidable_bijective_fintype Fintype.decidableBijectiveFintype
instance decidableRightInverseFintype [ DecidableEq : Sort ?u.51589 → Sort (max1?u.51589) α ] [ Fintype α ] ( f : α → β ) ( g : β → α ) :
Decidable ( Function.RightInverse : {α : Sort ?u.51610} → {β : Sort ?u.51609} → (β → α (α → β Prop f g ) :=
show Decidable (∀ x , g ( f x ) = x ) by infer_instance
#align fintype.decidable_right_inverse_fintype Fintype.decidableRightInverseFintype
instance decidableLeftInverseFintype : [inst : DecidableEq β [inst :