Documentation

Mathlib.Data.Finset.Option

Finite sets in Option α #

In this file we define

Then we prove some basic lemmas about these definitions.

Tags #

finset, option

def Option.toFinset {α : Type u_1} (o : Option α) :

Construct an empty or singleton finset from an Option

Equations
  • o.toFinset = o.elim singleton
Instances For
    @[simp]
    theorem Option.toFinset_none {α : Type u_1} :
    none.toFinset =
    @[simp]
    theorem Option.toFinset_some {α : Type u_1} {a : α} :
    (some a).toFinset = {a}
    @[simp]
    theorem Option.mem_toFinset {α : Type u_1} {a : α} {o : Option α} :
    a o.toFinset a o
    theorem Option.card_toFinset {α : Type u_1} (o : Option α) :
    o.toFinset.card = o.elim 0 1
    def Finset.insertNone {α : Type u_1} :

    Given a finset on α, lift it to being a finset on Option α using Option.some and then insert Option.none.

    Equations
    Instances For
      @[simp]
      theorem Finset.mem_insertNone {α : Type u_1} {s : Finset α} {o : Option α} :
      o Finset.insertNone s ao, a s
      theorem Finset.forall_mem_insertNone {α : Type u_1} {s : Finset α} {p : Option αProp} :
      (∀ aFinset.insertNone s, p a) p none as, p (some a)
      theorem Finset.some_mem_insertNone {α : Type u_1} {s : Finset α} {a : α} :
      some a Finset.insertNone s a s
      theorem Finset.none_mem_insertNone {α : Type u_1} {s : Finset α} :
      none Finset.insertNone s
      theorem Finset.insertNone_nonempty {α : Type u_1} {s : Finset α} :
      (Finset.insertNone s).Nonempty
      @[simp]
      theorem Finset.card_insertNone {α : Type u_1} (s : Finset α) :
      (Finset.insertNone s).card = s.card + 1
      def Finset.eraseNone {α : Type u_1} :

      Given s : Finset (Option α), eraseNone s : Finset α is the set of x : α such that some x ∈ s.

      Equations
      Instances For
        @[simp]
        theorem Finset.mem_eraseNone {α : Type u_1} {s : Finset (Option α)} {x : α} :
        x Finset.eraseNone s some x s
        theorem Finset.forall_mem_eraseNone {α : Type u_1} {s : Finset (Option α)} {p : Option αProp} :
        (∀ aFinset.eraseNone s, p (some a)) ∀ (a : α), some a sp (some a)
        theorem Finset.eraseNone_eq_biUnion {α : Type u_1} [DecidableEq α] (s : Finset (Option α)) :
        Finset.eraseNone s = s.biUnion Option.toFinset
        @[simp]
        theorem Finset.eraseNone_map_some {α : Type u_1} (s : Finset α) :
        Finset.eraseNone (Finset.map Function.Embedding.some s) = s
        @[simp]
        theorem Finset.eraseNone_image_some {α : Type u_1} [DecidableEq (Option α)] (s : Finset α) :
        Finset.eraseNone (Finset.image some s) = s
        @[simp]
        theorem Finset.coe_eraseNone {α : Type u_1} (s : Finset (Option α)) :
        (Finset.eraseNone s) = some ⁻¹' s
        @[simp]
        theorem Finset.eraseNone_union {α : Type u_1} [DecidableEq (Option α)] [DecidableEq α] (s : Finset (Option α)) (t : Finset (Option α)) :
        Finset.eraseNone (s t) = Finset.eraseNone s Finset.eraseNone t
        @[simp]
        theorem Finset.eraseNone_inter {α : Type u_1} [DecidableEq (Option α)] [DecidableEq α] (s : Finset (Option α)) (t : Finset (Option α)) :
        Finset.eraseNone (s t) = Finset.eraseNone s Finset.eraseNone t
        @[simp]
        theorem Finset.eraseNone_empty {α : Type u_1} :
        Finset.eraseNone =
        @[simp]
        theorem Finset.eraseNone_none {α : Type u_1} :
        Finset.eraseNone {none} =
        @[simp]
        theorem Finset.image_some_eraseNone {α : Type u_1} [DecidableEq (Option α)] (s : Finset (Option α)) :
        Finset.image some (Finset.eraseNone s) = s.erase none
        @[simp]
        theorem Finset.map_some_eraseNone {α : Type u_1} [DecidableEq (Option α)] (s : Finset (Option α)) :
        Finset.map Function.Embedding.some (Finset.eraseNone s) = s.erase none
        @[simp]
        theorem Finset.insertNone_eraseNone {α : Type u_1} [DecidableEq (Option α)] (s : Finset (Option α)) :
        Finset.insertNone (Finset.eraseNone s) = insert none s
        @[simp]
        theorem Finset.eraseNone_insertNone {α : Type u_1} (s : Finset α) :
        Finset.eraseNone (Finset.insertNone s) = s