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
Instances For
    @[simp]
    theorem Option.toFinset_none {α : Type u_1} :
    @[simp]
    theorem Option.toFinset_some {α : Type u_1} {a : α} :
    @[simp]
    theorem Option.mem_toFinset {α : Type u_1} {a : α} {o : Option α} :
    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
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem Finset.mem_insertNone {α : Type u_1} {s : Finset α} {o : Option α} :
      o Finset.insertNone s ∀ (a : α), a oa s
      theorem Finset.some_mem_insertNone {α : Type u_1} {s : Finset α} {a : α} :
      some a Finset.insertNone s a s
      @[simp]
      theorem Finset.card_insertNone {α : Type u_1} (s : Finset α) :
      Finset.card (Finset.insertNone s) = Finset.card s + 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
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem Finset.mem_eraseNone {α : Type u_1} {s : Finset (Option α)} {x : α} :
        x Finset.eraseNone s some x s
        theorem Finset.eraseNone_eq_biUnion {α : Type u_1} [DecidableEq α] (s : Finset (Option α)) :
        Finset.eraseNone s = Finset.biUnion s 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) = Finset.erase s none
        @[simp]
        theorem Finset.map_some_eraseNone {α : Type u_1} [DecidableEq (Option α)] (s : Finset (Option α)) :
        Finset.map Function.Embedding.some (Finset.eraseNone s) = Finset.erase s 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