Lattice

📁 Source: Mathlib/Data/List/Lattice.lean

Statistics

Metric	Count
Definitions	0
Theorems inter_eq_nil, inter_eq_left, union_eq_right, bagInter_nil, bagInter_nil_iff_inter_nil, bagInter_sublist_left, cons_bagInteger, cons_bagInter_of_neg, cons_bagInter_of_pos, count_bagInter, forall_mem_inter_of_forall_left, forall_mem_inter_of_forall_right, forall_mem_of_forall_mem_union_left, forall_mem_of_forall_mem_union_right, forall_mem_union, inter_cons, inter_cons_of_mem, inter_cons_of_notMem, inter_eq_nil_iff_disjoint, inter_nil, inter_nil', inter_reverse, inter_subset_left, inter_subset_right, mem_bagInter, mem_inter_of_mem_of_mem, mem_of_mem_inter_left, mem_of_mem_inter_right, mem_union_left, mem_union_right, nil_bagInter, sublist_suffix_of_union, subset_inter, suffix_union_right, union_sublist_append	35
Total	35

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bagInter_nil 📖	—	—	—	—	—
bagInter_nil_iff_inter_nil 📖	—	—	—	—	nil_bagInter cons_bagInter_of_pos inter_cons_of_mem cons_bagInter_of_neg inter_cons_of_notMem
bagInter_sublist_left 📖	—	—	—	—	bagInter.induct_unfolding
cons_bagInteger 📖	—	—	—	—	cons_bagInter_of_pos cons_bagInter_of_neg
cons_bagInter_of_neg 📖	—	—	—	—	—
cons_bagInter_of_pos 📖	—	—	—	—	—
count_bagInter 📖	—	—	—	—	bagInter.induct_unfolding
forall_mem_inter_of_forall_left 📖	—	—	—	—	BAll.imp_left mem_of_mem_inter_left
forall_mem_inter_of_forall_right 📖	—	—	—	—	BAll.imp_left mem_of_mem_inter_right
forall_mem_of_forall_mem_union_left 📖	—	—	—	—	forall_mem_union
forall_mem_of_forall_mem_union_right 📖	—	—	—	—	forall_mem_union
forall_mem_union 📖	—	—	—	—	—
inter_cons 📖	—	—	—	—	inter_cons_of_mem inter_cons_of_notMem
inter_cons_of_mem 📖	—	—	—	—	—
inter_cons_of_notMem 📖	—	—	—	—	—
inter_eq_nil_iff_disjoint 📖	—	—	—	—	—
inter_nil 📖	—	—	—	—	—
inter_nil' 📖	—	—	—	—	—
inter_reverse 📖	—	—	—	—	—
inter_subset_left 📖	—	—	—	—	filter_subset'
inter_subset_right 📖	—	—	—	—	mem_of_mem_inter_right
mem_bagInter 📖	—	—	—	—	bagInter.induct_unfolding
mem_inter_of_mem_of_mem 📖	—	—	—	—	mem_filter_of_mem
mem_of_mem_inter_left 📖	—	—	—	—	mem_of_mem_filter
mem_of_mem_inter_right 📖	—	—	—	—	of_mem_filter
mem_union_left 📖	—	—	—	—	—
mem_union_right 📖	—	—	—	—	—
nil_bagInter 📖	—	—	—	—	—
sublist_suffix_of_union 📖	—	—	—	—	sublist_cons_of_sublist Sublist.cons_cons
subset_inter 📖	—	—	—	—	—
suffix_union_right 📖	—	—	—	—	sublist_suffix_of_union
union_sublist_append 📖	—	—	—	—	sublist_suffix_of_union

List.Disjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inter_eq_nil 📖	—	—	—	—	List.inter_eq_nil_iff_disjoint

List.Subset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inter_eq_left 📖	—	—	—	—	—
union_eq_right 📖	—	—	—	—	List.mem_union_right

---

← Back to Index