@[simp]

theorem Hex.GraphIso.Nauty.VSet.card_empty {n : Nat} : empty.card = 0

@[simp]

theorem Hex.GraphIso.Nauty.VSet.inter_empty {n : Nat} (s : VSet n) : s.inter empty = empty

@[simp]

theorem Hex.GraphIso.Nauty.VSet.empty_inter {n : Nat} (s : VSet n) : empty.inter s = empty

@[simp]

theorem Hex.GraphIso.Nauty.VSet.union_empty {n : Nat} (s : VSet n) : s.union empty = s

@[simp]

theorem Hex.GraphIso.Nauty.VSet.empty_union {n : Nat} (s : VSet n) : empty.union s = s

theorem Hex.GraphIso.Nauty.VSet.inter_self {n : Nat} (s : VSet n) : s.inter s = s

theorem Hex.GraphIso.Nauty.VSet.card_union_disjoint {n : Nat} {a b : VSet n} (hd : a.inter b = empty) : (a.union b).card = a.card + b.card

Member counts add over a disjoint union.

theorem Hex.GraphIso.Nauty.VSet.inter_union_distrib {n : Nat} (a b x : VSet n) : (a.union b).inter x = (a.inter x).union (b.inter x)

theorem Hex.GraphIso.Nauty.VSet.cardInter_union_disjoint {n : Nat} {a b : VSet n} (hd : a.inter b = empty) (x : VSet n) : (a.union b).cardInter x = a.cardInter x + b.cardInter x

Counts into a set add over a disjoint union.

theorem Hex.GraphIso.Nauty.VSet.mem_singleton {n : Nat} (u v : Nat) : (empty.insert u).mem v = (u == v && decide (u < n))

theorem Hex.GraphIso.Nauty.VSet.inter_comm {n : Nat} (s t : VSet n) : s.inter t = t.inter s

theorem Hex.GraphIso.Nauty.VSet.union_comm {n : Nat} (s t : VSet n) : s.union t = t.union s

theorem Hex.GraphIso.Nauty.VSet.union_assoc {n : Nat} (s t u : VSet n) : (s.union t).union u = s.union (t.union u)

theorem Hex.GraphIso.Nauty.VSet.cardInter_comm {n : Nat} (s t : VSet n) : s.cardInter t = t.cardInter s

theorem Hex.GraphIso.Nauty.VSet.cardInter_singleton {n : Nat} (u : Nat) (x : VSet n) : (empty.insert u).cardInter x = if x.mem u = true then 1 else 0

The count into a singleton is the membership bit.

theorem Hex.GraphIso.Nauty.VSet.countP_le_of_imp {α : Type u_1} {p q : α → Bool} {l : List α} : (∀ (x : α), x ∈ l → p x = true → q x = true) → List.countP p l ≤ List.countP q l

countP is monotone under pointwise implication of the predicate on the list's elements.

theorem Hex.GraphIso.Nauty.VSet.filter_eq_of_imp_of_length_eq {α : Type u_1} {p q : α → Bool} {l : List α} (himp : ∀ (x : α), x ∈ l → p x = true → q x = true) (hlen : (List.filter p l).length = (List.filter q l).length) : List.filter p l = List.filter q l

Two filters ordered by pointwise implication are equal when they have the same length.

theorem Hex.GraphIso.Nauty.VSet.card_le_of_subset {n : Nat} {s t : VSet n} (h : s.subset t = true) : s.card ≤ t.card

A subset has no more members.

theorem Hex.GraphIso.Nauty.VSet.eq_empty_of_card_eq_zero {n : Nat} {s : VSet n} (h : s.card = 0) : s = empty

A set with no members is empty.

theorem Hex.GraphIso.Nauty.VSet.eq_of_subset_of_card_eq {n : Nat} {s t : VSet n} (h : s.subset t = true) (hcard : s.card = t.card) : s = t

A subset with the same member count is the whole set.

theorem Hex.GraphIso.Nauty.VSet.countBelow_succ {n : Nat} (s : VSet n) (k : Nat) : s.countBelow (k + 1) = s.countBelow k + if s.mem k = true then 1 else 0

theorem Hex.GraphIso.Nauty.VSet.countBelow_congr {n : Nat} {s t : VSet n} {k : Nat} (h : ∀ (i : Nat), i < k → s.mem i = t.mem i) : s.countBelow k = t.countBelow k

theorem Hex.GraphIso.Nauty.VSet.countBelow_le {n : Nat} (s : VSet n) (k : Nat) : s.countBelow k ≤ k

theorem Hex.GraphIso.Nauty.VSet.card_le {n : Nat} (s : VSet n) : s.card ≤ n

A set has at most n members.

theorem Hex.GraphIso.Nauty.VSet.countBelow_insert_le {n : Nat} (s : VSet n) (v k : Nat) : (s.insert v).countBelow k ≤ s.countBelow k + 1

theorem Hex.GraphIso.Nauty.VSet.card_insert_le {n : Nat} (s : VSet n) (v : Nat) : (s.insert v).card ≤ s.card + 1

Inserting adds at most one member.

theorem Hex.GraphIso.Nauty.VSet.countBelow_erase_of_mem {n : Nat} {s : VSet n} {v : Nat} (h : s.mem v = true) (k : Nat) : v < k → (s.erase v).countBelow k + 1 = s.countBelow k

theorem Hex.GraphIso.Nauty.VSet.card_erase_of_mem {n : Nat} {s : VSet n} {v : Nat} (h : s.mem v = true) : (s.erase v).card + 1 = s.card

Erasing a member removes exactly one.

theorem Hex.GraphIso.Nauty.VSet.card_erase_le {n : Nat} (s : VSet n) (v : Nat) : (s.erase v).card ≤ s.card

Erasing never adds members.

theorem Hex.GraphIso.Nauty.VSet.insert_of_mem {n : Nat} {s : VSet n} {v : Nat} (h : s.mem v = true) : s.insert v = s

Inserting a member changes nothing.