Disjoint finite sets #
Main declarations #
Disjoint
: defined via the lattice structure on finsets; two sets are disjoint if their intersection is empty.Finset.disjUnion
: the union of the finite setss
andt
, given a proofDisjoint s t
Tags #
finite sets, finset
disjoint #
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
Equations
disjoint union #
@[simp]
@[simp]
@[simp]
insert #
@[simp]
@[simp]
@[simp]