Empty and nonempty finite sets #
This file defines the empty finite set ∅ and a predicate for nonempty Finset
s.
Main declarations #
Finset.Nonempty
: A finset is nonempty if it has elements. This is equivalent to sayings ≠ ∅
.Finset.empty
: Denoted by∅
. The finset associated to any type consisting of no elements.
Tags #
finite sets, finset
Nonempty #
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.
Instances For
Alias of the reverse direction of Finset.coe_nonempty
.
Alias of the reverse direction of Finset.nonempty_coe_sort
.
@[deprecated Finset.Nonempty.exists_mem]
Alias of Finset.Nonempty.exists_mem
.
theorem
Finset.Nonempty.mono
{α : Type u_1}
{s t : Finset α}
(hst : s ⊆ t)
(hs : s.Nonempty)
:
t.Nonempty
empty #
Equations
- Finset.instEmptyCollection = { emptyCollection := Finset.empty }
Equations
- Finset.instOrderBot = OrderBot.mk ⋯
Alias of the reverse direction of Finset.empty_ssubset
.
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 oraesop 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.