Small Finset and Set Helpers

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

@[reducible, inline]

noncomputable abbrev Utils.oneIf (P : Prop) : ℤ

The integer-valued indicator of a proposition: 1 when P holds and 0 otherwise. This is the paper's notation δ[P].

Equations

• Utils.oneIf P = if P then 1 else 0

theorem Utils.oneIf_congr {P Q : Prop} (h : P ↔ Q) : oneIf P = oneIf Q

The indicator δ[P] depends only on the truth value of P.

theorem Utils.oneIf_Ico_eq_sub (m n : ℤ) (m_le_n : m ≤ n) (k : ℤ) : oneIf (k ∈ Finset.Ico m n) = oneIf (k < n) - oneIf (k < m)

On an integer interval, membership is the difference of two initial segments.

theorem Utils.sum_oneIf_mem_of_subset {ι : Type u_1} {A U : Finset ι} (hAU : A ⊆ U) : ∑ k ∈ U, oneIf (k ∈ A) = ↑A.card

Summing the indicator of membership in A over any finite superset U counts A.

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

• ⋯ = ⋯