Documentation

Mathlib.Data.Set.Finite.Monad

Finiteness of the Set monad operations #

Tags #

finite sets

Fintype instances #

Every instance here should have a corresponding Set.Finite constructor in the next section.

source
def Set.fintypeBind {α β : Type u_1} [DecidableEq β] (s : Set α) [Fintype ↑s] (f : α → Set β) (H : (a : α) → a ∈ s → Fintype ↑(f a)) :
Fintype ↑(s >>= f)

If s : Set α is a set with Fintype instance and f : α → Set β is a function such that each f a, a ∈ s, has a Fintype structure, then s >>= f has a Fintype structure.

Equations
  • s.fintypeBind f H = s.fintypeBiUnion f H
Instances For
    source
    instance Set.fintypeBind' {α β : Type u_1} [DecidableEq β] (s : Set α) [Fintype ↑s] (f : α → Set β) [(a : α) → Fintype ↑(f a)] :
    Fintype ↑(s >>= f)
    Equations
    • s.fintypeBind' f = s.fintypeBiUnion' f
    source
    instance Set.fintypePure {α : Type u} (a : α) :
    Fintype ↑(pure a)
    Equations
    • Set.fintypePure = Set.fintypeSingleton
    source
    instance Set.fintypeSeq {α : Type u} {β : Type v} [DecidableEq β] (f : Set (α → β)) (s : Set α) [Fintype ↑f] [Fintype ↑s] :
    Fintype ↑(f.seq s)
    Equations
    • f.fintypeSeq s = ⋯.mpr (f.fintypeBiUnion' fun (x : α → β) => x '' s)
    source
    instance Set.fintypeSeq' {α β : Type u} [DecidableEq β] (f : Set (α → β)) (s : Set α) [Fintype ↑f] [Fintype ↑s] :
    Fintype ↑(f <*> s)
    Equations
    • f.fintypeSeq' s = f.fintypeSeq s

    Finite instances #

    There is seemingly some overlap between the following instances and the Fintype instances in Data.Set.Finite. While every Fintype instance gives a Finite instance, those instances that depend on Fintype or Decidable instances need an additional Finite instance to be able to generally apply.

    Some set instances do not appear here since they are consequences of others, for example Subtype.Finite for subsets of a finite type.

    source
    theorem Finite.Set.finite_pure {α : Type u} (a : α) :
    (pure a).Finite
    source
    instance Finite.Set.finite_seq {α : Type u} {β : Type v} (f : Set (α → β)) (s : Set α) [Finite ↑f] [Finite ↑s] :
    Finite ↑(f.seq s)
    Equations
    • ⋯ = ⋯

    Constructors for Set.Finite #

    Every constructor here should have a corresponding Fintype instance in the previous section (or in the Fintype module).

    The implementation of these constructors ideally should be no more than Set.toFinite, after possibly setting up some Fintype and classical Decidable instances.

    source
    theorem Set.Finite.bind {α β : Type u_1} {s : Set α} {f : α → Set β} (h : s.Finite) (hf : ∀ a ∈ s, (f a).Finite) :
    (s >>= f).Finite
    source
    theorem Set.Finite.seq {α : Type u} {β : Type v} {f : Set (α → β)} {s : Set α} (hf : f.Finite) (hs : s.Finite) :
    (f.seq s).Finite
    source
    theorem Set.Finite.seq' {α β : Type u} {f : Set (α → β)} {s : Set α} (hf : f.Finite) (hs : s.Finite) :
    (f <*> s).Finite