Small Finset and Set Helpers

This namespace contains auxiliary lemmas used across the development but not specific to ASP permutations or Demazure product.

theorem Utils.sub_card_eq_sub_card_diff (S T : Finset ℤ) : ↑S.card - ↑T.card = ↑(S \ T).card - ↑(T \ S).card

The difference of the cardinalities of two finite sets is equal to the difference of the cardinalities of their set-theoretic differences.

theorem Utils.card_filter_helper (S : Finset ℤ) (f : ℤ → ℤ) (c : ℤ) : {x ∈ S | f x ≥ c}.card + {x ∈ S | f x < c}.card = S.card

@[irreducible]

def Utils.min_helper {m n : ℤ} (m_pos : m ≥ 1) (n_pos : n ≥ 1) {S : Set (ℤ × ℤ)} (mem : (m, n) ∈ S) (nmem : (1, 1) ∉ S) : ∃ (m' : ℤ) (n' : ℤ), m' ≥ 1 ∧ n' ≥ 1 ∧ (m', n') ∈ S ∧ ((m' - 1, n') ∉ S ∧ m' ≥ 2 ∨ (m', n' - 1) ∉ S ∧ n' ≥ 2)

Equations

• ⋯ = ⋯