Documentation

Mathlib.Data.Finset.Empty

Empty and nonempty finite sets #

This file defines the empty finite set ∅ and a predicate for nonempty Finsets.

Main declarations #

Tags #

finite sets, finset

Nonempty #

def Finset.Nonempty {α : Type u_1} (s : Finset α) :

The property s.Nonempty expresses the fact that the finset s is not empty. It should be used in theorem assumptions instead of ∃ x, x ∈ s or s ≠ ∅ as it gives access to a nice API thanks to the dot notation.

Equations
  • s.Nonempty = ∃ (x : α), x s
Instances For
    instance Finset.decidableNonempty {α : Type u_1} {s : Finset α} :
    Decidable s.Nonempty
    Equations
    @[simp]
    theorem Finset.coe_nonempty {α : Type u_1} {s : Finset α} :
    (↑s).Nonempty s.Nonempty
    theorem Finset.nonempty_coe_sort {α : Type u_1} {s : Finset α} :
    Nonempty { x : α // x s } s.Nonempty
    theorem Finset.Nonempty.to_set {α : Type u_1} {s : Finset α} :
    s.Nonempty(↑s).Nonempty

    Alias of the reverse direction of Finset.coe_nonempty.

    theorem Finset.Nonempty.coe_sort {α : Type u_1} {s : Finset α} :
    s.NonemptyNonempty { x : α // x s }

    Alias of the reverse direction of Finset.nonempty_coe_sort.

    theorem Finset.Nonempty.exists_mem {α : Type u_1} {s : Finset α} (h : s.Nonempty) :
    ∃ (x : α), x s
    @[deprecated Finset.Nonempty.exists_mem]
    theorem Finset.Nonempty.bex {α : Type u_1} {s : Finset α} (h : s.Nonempty) :
    ∃ (x : α), x s

    Alias of Finset.Nonempty.exists_mem.

    theorem Finset.Nonempty.mono {α : Type u_1} {s t : Finset α} (hst : s t) (hs : s.Nonempty) :
    t.Nonempty
    theorem Finset.Nonempty.forall_const {α : Type u_1} {s : Finset α} (h : s.Nonempty) {p : Prop} :
    (∀ xs, p) p
    theorem Finset.Nonempty.to_subtype {α : Type u_1} {s : Finset α} :
    s.NonemptyNonempty { x : α // x s }
    theorem Finset.Nonempty.to_type {α : Type u_1} {s : Finset α} :
    s.NonemptyNonempty α

    empty #

    def Finset.empty {α : Type u_1} :

    The empty finset

    Equations
    • Finset.empty = { val := 0, nodup := }
    Instances For
      Equations
      • Finset.instEmptyCollection = { emptyCollection := Finset.empty }
      instance Finset.inhabitedFinset {α : Type u_1} :
      Equations
      • Finset.inhabitedFinset = { default := }
      @[simp]
      theorem Finset.empty_val {α : Type u_1} :
      .val = 0
      @[simp]
      theorem Finset.not_mem_empty {α : Type u_1} (a : α) :
      a
      @[simp]
      theorem Finset.not_nonempty_empty {α : Type u_1} :
      ¬.Nonempty
      @[simp]
      theorem Finset.mk_zero {α : Type u_1} :
      { val := 0, nodup := } =
      theorem Finset.ne_empty_of_mem {α : Type u_1} {a : α} {s : Finset α} (h : a s) :
      theorem Finset.Nonempty.ne_empty {α : Type u_1} {s : Finset α} (h : s.Nonempty) :
      @[simp]
      theorem Finset.empty_subset {α : Type u_1} (s : Finset α) :
      theorem Finset.eq_empty_of_forall_not_mem {α : Type u_1} {s : Finset α} (H : ∀ (x : α), xs) :
      s =
      theorem Finset.eq_empty_iff_forall_not_mem {α : Type u_1} {s : Finset α} :
      s = ∀ (x : α), xs
      @[simp]
      theorem Finset.val_eq_zero {α : Type u_1} {s : Finset α} :
      s.val = 0 s =
      @[simp]
      theorem Finset.subset_empty {α : Type u_1} {s : Finset α} :
      @[simp]
      theorem Finset.not_ssubset_empty {α : Type u_1} (s : Finset α) :
      theorem Finset.nonempty_of_ne_empty {α : Type u_1} {s : Finset α} (h : s ) :
      s.Nonempty
      theorem Finset.nonempty_iff_ne_empty {α : Type u_1} {s : Finset α} :
      s.Nonempty s
      @[simp]
      theorem Finset.not_nonempty_iff_eq_empty {α : Type u_1} {s : Finset α} :
      ¬s.Nonempty s =
      theorem Finset.eq_empty_or_nonempty {α : Type u_1} (s : Finset α) :
      s = s.Nonempty
      @[simp]
      theorem Finset.coe_empty {α : Type u_1} :
      =
      @[simp]
      theorem Finset.coe_eq_empty {α : Type u_1} {s : Finset α} :
      s = s =
      theorem Finset.isEmpty_coe_sort {α : Type u_1} {s : Finset α} :
      IsEmpty { x : α // x s } s =
      instance Finset.instIsEmpty {α : Type u_1} :
      IsEmpty { x : α // x }
      Equations
      • =
      theorem Finset.eq_empty_of_isEmpty {α : Type u_1} [IsEmpty α] (s : Finset α) :
      s =

      A Finset for an empty type is empty.

      instance Finset.instOrderBot {α : Type u_1} :
      Equations
      @[simp]
      theorem Finset.bot_eq_empty {α : Type u_1} :
      @[simp]
      theorem Finset.empty_ssubset {α : Type u_1} {s : Finset α} :
      s s.Nonempty
      theorem Finset.Nonempty.empty_ssubset {α : Type u_1} {s : Finset α} :
      s.Nonempty s

      Alias of the reverse direction of Finset.empty_ssubset.

      theorem Finset.exists_mem_empty_iff {α : Type u_1} (p : αProp) :
      (∃ x, p x) False
      theorem Finset.forall_mem_empty_iff {α : Type u_1} (p : αProp) :
      (∀ x, p x) True
      def Mathlib.Meta.proveFinsetNonempty {u : Lean.Level} {α : Q(Type u)} (s : Q(Finset «$α»)) :
      Lean.MetaM (Option Q(«$s».Nonempty))

      Attempt to prove that a finset is nonempty using the finsetNonempty aesop rule-set.

      You can add lemmas to the rule-set by tagging them with either:

      • aesop safe apply (rule_sets := [finsetNonempty]) if they are always a good idea to follow or
      • aesop unsafe apply (rule_sets := [finsetNonempty]) if they risk directing the search to a blind alley.

      TODO: should some of the lemmas be aesop safe simp instead?

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For