Skew shapes and their associated 321-avoiding permutations

IOU more description here.

def SkewShapes.Δ : ℤ × ℤ → ℤ

The content $j - i$ of the box $(i,j)$.

Equations

• SkewShapes.Δ (i, j) = j - i

theorem SkewShapes.Δ_eq (x : ℤ × ℤ) : Δ x = x.2 - x.1

def SkewShapes.flip : ℤ × ℤ → ℤ × ℤ

Reflection through the line $y = -x$, sending $(i,j)$ to $(-j,-i)$.

Equations

• SkewShapes.flip (i, j) = (-j, -i)

@[simp]

theorem SkewShapes.flip_flip (x : ℤ × ℤ) : flip (flip x) = x

theorem SkewShapes.flip_involutive : Function.Involutive flip

theorem SkewShapes.le_flip {x y : ℤ × ℤ} : x ≤ flip y ↔ y ≤ flip x

theorem SkewShapes.flip_le {x y : ℤ × ℤ} : flip x ≤ y ↔ flip y ≤ x

@[simp]

theorem SkewShapes.flip_le_flip {x y : ℤ × ℤ} : flip x ≤ flip y ↔ y ≤ x

@[simp]

theorem SkewShapes.flip_fst (x : ℤ × ℤ) : (flip x).1 = -x.2

@[simp]

theorem SkewShapes.flip_snd (x : ℤ × ℤ) : (flip x).2 = -x.1

@[simp]

theorem SkewShapes.flip_mk (i j : ℤ) : flip (i, j) = (-j, -i)

theorem SkewShapes.flip_add (x y : ℤ × ℤ) : flip (x + y) = flip x + flip y

theorem SkewShapes.flip_sub (x y : ℤ × ℤ) : flip (x - y) = flip x - flip y

@[simp]

theorem SkewShapes.Δ_flip (x : ℤ × ℤ) : Δ (flip x) = Δ x

theorem SkewShapes.Δ_add_fst (x : ℤ × ℤ) : Δ (x + (1, 0)) = Δ x - 1

theorem SkewShapes.Δ_add_snd (x : ℤ × ℤ) : Δ (x + (0, 1)) = Δ x + 1

structure SkewShapes.SkewShape : Type

A skew shape: a convex set of boxes in $\mathbb{Z} \times \mathbb{Z}$, in matrix coordinates (row $i$ increasing southward, column $j$ increasing eastward), such that each box has only finitely many boxes weakly northwest and weakly southeast of it.

• boxes : Set (ℤ × ℤ)
• closed (x y z : ℤ × ℤ) : x ≤ y → y ≤ z → x ∈ self.boxes → z ∈ self.boxes → y ∈ self.boxes
• finite_below (x : ℤ × ℤ) : x ∈ self.boxes → Finite ↑{y : ℤ × ℤ | y ∈ self.boxes ∧ y ≤ x}
• finite_above (x : ℤ × ℤ) : x ∈ self.boxes → Finite ↑{y : ℤ × ℤ | y ∈ self.boxes ∧ x ≤ y}

@[instance_reducible]

instance SkewShapes.instSetLikeSkewShapeProdInt : SetLike SkewShape (ℤ × ℤ)

Equations

• SkewShapes.instSetLikeSkewShapeProdInt = { coe := SkewShapes.SkewShape.boxes, coe_injective := SkewShapes.instSetLikeSkewShapeProdInt._proof_1 }

def SkewShapes.SkewShape.flip (S : SkewShape) : SkewShape

The reflection of $S$ through the line $y = -x$.

Equations

• S.flip = { boxes := SkewShapes.flip '' S.boxes, closed := ⋯, finite_below := ⋯, finite_above := ⋯ }

@[simp]

theorem SkewShapes.SkewShape.flip_mem_flip (S : SkewShape) {x : ℤ × ℤ} : flip x ∈ S.flip ↔ x ∈ S

def SkewShapes.SkewShape.flipBox (S : SkewShape) (x : ↥S) : ↥S.flip

The box of the flipped shape obtained by reflecting a box of $S$.

Equations

• S.flipBox x = ⟨SkewShapes.flip ↑x, ⋯⟩

@[simp]

theorem SkewShapes.SkewShape.flipBox_val (S : SkewShape) (x : ↥S) : ↑(S.flipBox x) = flip ↑x

theorem SkewShapes.SkewShape.mem_flip (S : SkewShape) {y : ℤ × ℤ} : y ∈ S.flip ↔ flip y ∈ S

theorem SkewShapes.SkewShape.flipBox_bijective (S : SkewShape) : Function.Bijective S.flipBox

theorem SkewShapes.SkewShape.flip_flip (S : SkewShape) : S.flip.flip = S

def SkewShapes.SkewShape.support (S : SkewShape) : Set ℤ

The integers $\Delta(x)$ and $\Delta(x) + 1$ for boxes $x$ of $S$.

Equations

• S.support = SkewShapes.Δ '' S.boxes ∪ (fun (x : ℤ × ℤ) => SkewShapes.Δ x + 1) '' S.boxes

@[irreducible]

noncomputable def SkewShapes.SkewShape.U (S : SkewShape) (x : ↥S) : ℤ × ℤ

The southernmost box in the column of $x$.

Equations

• S.U x = if h : ↑x + (1, 0) ∈ S then S.U ⟨↑x + (1, 0), h⟩ else ↑x

@[irreducible]

noncomputable def SkewShapes.SkewShape.V (S : SkewShape) (x : ↥S) : ℤ × ℤ

The first box east of the row of $x$ that is not in $S$.

Equations

• S.V x = if h : ↑x + (0, 1) ∈ S then S.V ⟨↑x + (0, 1), h⟩ else ↑x + (0, 1)

noncomputable def SkewShapes.SkewShape.U' (S : SkewShape) (x : ↥S) : ℤ × ℤ

The westernmost box in the row of $x$ (the reflection of $U$).

Equations

• S.U' x = SkewShapes.flip (S.flip.U (S.flipBox x))

noncomputable def SkewShapes.SkewShape.V' (S : SkewShape) (x : ↥S) : ℤ × ℤ

The first box north of the column of $x$ that is not in $S$ (the reflection of $V$).

Equations

• S.V' x = SkewShapes.flip (S.flip.V (S.flipBox x))

@[reducible, inline]

noncomputable abbrev SkewShapes.SkewShape.u (S : SkewShape) (x : ↥S) : ℤ

Equations

• S.u x = SkewShapes.Δ (S.U x)

@[reducible, inline]

noncomputable abbrev SkewShapes.SkewShape.u' (S : SkewShape) (x : ↥S) : ℤ

Equations

• S.u' x = SkewShapes.Δ (S.U' x)

@[reducible, inline]

noncomputable abbrev SkewShapes.SkewShape.v (S : SkewShape) (x : ↥S) : ℤ

Equations

• S.v x = SkewShapes.Δ (S.V x)

@[reducible, inline]

noncomputable abbrev SkewShapes.SkewShape.v' (S : SkewShape) (x : ↥S) : ℤ

Equations

• S.v' x = SkewShapes.Δ (S.V' x)

def SkewShapes.SkewShape.I (S : SkewShape) : Set (ℤ × ℤ)

The pairs $(u(x), v(x))$ for $x \in S$; this is the inversion set of $\sigma$.

Equations

• S.I = {x : ℤ × ℤ | ∃ (x_1 : ↥S), (S.u x_1, S.v x_1) = x}

def SkewShapes.SkewShape.I' (S : SkewShape) : Set (ℤ × ℤ)

The pairs $(u'(x), v'(x))$ for $x \in S$.

Equations

• S.I' = {x : ℤ × ℤ | ∃ (x_1 : ↥S), (S.u' x_1, S.v' x_1) = x}

theorem SkewShapes.SkewShape.mem_I (S : SkewShape) {a b : ℤ} : (a, b) ∈ S.I ↔ ∃ (x : ↥S), S.u x = a ∧ S.v x = b

noncomputable def SkewShapes.SkewShape.pair (S : SkewShape) (x : ↥S) : ℤ × ℤ

The pair $(u(x), v(x))$ attached to a box $x$; these pairs make up $I$.

Equations

• S.pair x = (S.u x, S.v x)

theorem SkewShapes.SkewShape.I_eq_range_pair (S : SkewShape) : S.I = Set.range S.pair

theorem SkewShapes.SkewShape.U_spec (S : SkewShape) (x : ↥S) (y : ℤ × ℤ) : y = S.U x ↔ y.2 = (↑x).2 ∧ y ∈ S ∧ y + (1, 0) ∉ S

theorem SkewShapes.SkewShape.U_snd (S : SkewShape) (x : ↥S) : (S.U x).2 = (↑x).2

theorem SkewShapes.SkewShape.U_in_S (S : SkewShape) (x : ↥S) : S.U x ∈ S

theorem SkewShapes.SkewShape.U_add_not_in_S (S : SkewShape) (x : ↥S) : S.U x + (1, 0) ∉ S

theorem SkewShapes.SkewShape.U_fst (S : SkewShape) (x : ↥S) : (↑x).1 ≤ (S.U x).1

theorem SkewShapes.SkewShape.U'_spec (S : SkewShape) (x : ↥S) (y : ℤ × ℤ) : y = S.U' x ↔ y.1 = (↑x).1 ∧ y ∈ S ∧ y - (0, 1) ∉ S

theorem SkewShapes.SkewShape.U'_fst (S : SkewShape) (x : ↥S) : (S.U' x).1 = (↑x).1

theorem SkewShapes.SkewShape.U'_in_S (S : SkewShape) (x : ↥S) : S.U' x ∈ S

theorem SkewShapes.SkewShape.U'_sub_not_in_S (S : SkewShape) (x : ↥S) : S.U' x - (0, 1) ∉ S

theorem SkewShapes.SkewShape.U'_snd (S : SkewShape) (x : ↥S) : (S.U' x).2 ≤ (↑x).2

theorem SkewShapes.SkewShape.V_spec (S : SkewShape) (x : ↥S) (y : ℤ × ℤ) : y = S.V x ↔ y.1 = (↑x).1 ∧ y - (0, 1) ∈ S ∧ y ∉ S

theorem SkewShapes.SkewShape.V_fst (S : SkewShape) (x : ↥S) : (S.V x).1 = (↑x).1

theorem SkewShapes.SkewShape.V_sub_in_S (S : SkewShape) (x : ↥S) : S.V x - (0, 1) ∈ S

theorem SkewShapes.SkewShape.V_not_in_S (S : SkewShape) (x : ↥S) : S.V x ∉ S

theorem SkewShapes.SkewShape.V_snd (S : SkewShape) (x : ↥S) : (↑x).2 < (S.V x).2

theorem SkewShapes.SkewShape.V'_spec (S : SkewShape) (x : ↥S) (y : ℤ × ℤ) : y = S.V' x ↔ y.2 = (↑x).2 ∧ y + (1, 0) ∈ S ∧ y ∉ S

theorem SkewShapes.SkewShape.V'_snd (S : SkewShape) (x : ↥S) : (S.V' x).2 = (↑x).2

theorem SkewShapes.SkewShape.V'_add_in_S (S : SkewShape) (x : ↥S) : S.V' x + (1, 0) ∈ S

theorem SkewShapes.SkewShape.V'_not_in_S (S : SkewShape) (x : ↥S) : S.V' x ∉ S

theorem SkewShapes.SkewShape.V'_fst (S : SkewShape) (x : ↥S) : (S.V' x).1 < (↑x).1

Rows and columns

def SkewShapes.SkewShape.row (S : SkewShape) (x : ↥S) : Set ↥S

The boxes of $S$ in the row of $x$.

Equations

• S.row x = {y : ↥S | (↑y).1 = (↑x).1}

def SkewShapes.SkewShape.col (S : SkewShape) (x : ↥S) : Set ↥S

The boxes of $S$ in the column of $x$.

Equations

• S.col x = {y : ↥S | (↑y).2 = (↑x).2}

@[simp]

theorem SkewShapes.SkewShape.mem_row (S : SkewShape) {x y : ↥S} : y ∈ S.row x ↔ (↑y).1 = (↑x).1

@[simp]

theorem SkewShapes.SkewShape.mem_col (S : SkewShape) {x y : ↥S} : y ∈ S.col x ↔ (↑y).2 = (↑x).2

theorem SkewShapes.SkewShape.U_eq_U_iff (S : SkewShape) (x y : ↥S) : S.U y = S.U x ↔ (↑y).2 = (↑x).2

Two boxes have the same $U$ exactly when they lie in the same column.

theorem SkewShapes.SkewShape.V_eq_V_iff (S : SkewShape) (x y : ↥S) : S.V y = S.V x ↔ (↑y).1 = (↑x).1

Two boxes have the same $V$ exactly when they lie in the same row.

theorem SkewShapes.SkewShape.col_mem_iff (S : SkewShape) (x : ↥S) (i : ℤ) : (i, (↑x).2) ∈ S ↔ (S.V' x).1 < i ∧ i ≤ (S.U x).1

The column of $x$ runs from just south of $V'(x)$ down to $U(x)$.

theorem SkewShapes.SkewShape.row_mem_iff (S : SkewShape) (x : ↥S) (j : ℤ) : ((↑x).1, j) ∈ S ↔ (S.U' x).2 ≤ j ∧ j < (S.V x).2

The row of $x$ runs from $U'(x)$ east to just west of $V(x)$.

theorem SkewShapes.SkewShape.col_finite (S : SkewShape) (x : ↥S) : (S.col x).Finite

theorem SkewShapes.SkewShape.row_finite (S : SkewShape) (x : ↥S) : (S.row x).Finite

theorem SkewShapes.SkewShape.col_ncard (S : SkewShape) (x : ↥S) : ↑(S.col x).ncard = (S.U x).1 - (S.V' x).1

theorem SkewShapes.SkewShape.row_ncard (S : SkewShape) (x : ↥S) : ↑(S.row x).ncard = (S.V x).2 - (S.U' x).2

theorem SkewShapes.SkewShape.support_convexity (S : SkewShape) (x : ↥S) (n : ℤ) : S.u x ≤ n → n ≤ S.v x → n ∈ S.support

theorem SkewShapes.SkewShape.u_le_Δ (S : SkewShape) (x : ↥S) : S.u x ≤ Δ ↑x

theorem SkewShapes.SkewShape.Δ_lt_v (S : SkewShape) (x : ↥S) : Δ ↑x < S.v x

noncomputable def SkewShapes.SkewShape.fringe (S : SkewShape) : Set (ℤ × ℤ)

The boxes $U(x)$ and $V(x)$ for $x \in S$.

Equations

• S.fringe = Set.range S.U ∪ Set.range S.V

theorem SkewShapes.SkewShape.U_fringe (S : SkewShape) (x : ↥S) : S.U x ∈ S.fringe

theorem SkewShapes.SkewShape.V_fringe (S : SkewShape) (x : ↥S) : S.V x ∈ S.fringe

noncomputable def SkewShapes.SkewShape.fringe' (S : SkewShape) : Set (ℤ × ℤ)

Equations

• S.fringe' = Set.range S.U' ∪ Set.range S.V'

noncomputable def SkewShapes.SkewShape.fringe_flip (S : SkewShape) (x : ↑S.fringe) : ↑S.fringe'

Equations

• S.fringe_flip x = if h : ↑x ∈ Set.range S.U then ⟨S.V' (Classical.choose h), ⋯⟩ else have h' := ⋯; ⟨S.U' (Classical.choose h'), ⋯⟩

def SkewShapes.SkewShape.down_closure (S : SkewShape) : Set (ℤ × ℤ)

Equations

• S.down_closure = {x : ℤ × ℤ | ∃ y ∈ S, x ≤ y}

def SkewShapes.SkewShape.ext_fringe (S : SkewShape) : Set (ℤ × ℤ)

Equations

• S.ext_fringe = {x : ℤ × ℤ | x - (0, 1) ∈ S.down_closure ∧ x + (1, 0) ∉ S.down_closure}

theorem SkewShapes.SkewShape.mem_down_closure_of_le (S : SkewShape) {x y : ℤ × ℤ} (hy : y ∈ S.down_closure) (hxy : x ≤ y) : x ∈ S.down_closure

theorem SkewShapes.SkewShape.mem_down_closure (S : SkewShape) {x : ℤ × ℤ} (hx : x ∈ S) : x ∈ S.down_closure

theorem SkewShapes.SkewShape.ext_fringe_inj (S : SkewShape) {x y : ℤ × ℤ} (hx : x ∈ S.ext_fringe) (hy : y ∈ S.ext_fringe) (h : Δ x = Δ y) : x = y

A box of the extended fringe is determined by its content.

theorem SkewShapes.SkewShape.exists_ext_fringe (S : SkewShape) (hS : S.boxes.Nonempty) (n : ℤ) : ∃ x ∈ S.ext_fringe, Δ x = n

A nonempty skew shape has an extended fringe box of each content.

theorem SkewShapes.SkewShape.U_add_mem_ext_fringe (S : SkewShape) (x : ↥S) : S.U x + (0, 1) ∈ S.ext_fringe

The box east of $U(x)$ lies on the extended fringe.

theorem SkewShapes.SkewShape.V_sub_mem_ext_fringe (S : SkewShape) (x : ↥S) : S.V x - (1, 0) ∈ S.ext_fringe

The box north of $V(x)$ lies on the extended fringe.

theorem SkewShapes.SkewShape.fringe_crit (S : SkewShape) (x : ℤ × ℤ) : x ∈ S.fringe → x ∈ S.ext_fringe

theorem SkewShapes.SkewShape.fringe_inj (S : SkewShape) {x y : ℤ × ℤ} (hx : x ∈ S.fringe) (hy : y ∈ S.fringe) (h : Δ x = Δ y) : x = y

A fringe box is determined by its content.

theorem SkewShapes.SkewShape.support_fringe (S : SkewShape) (n : ↑S.support) : ∃! y : ↑S.fringe, Δ ↑y = ↑n

theorem SkewShapes.SkewShape.support_spec (S : SkewShape) : S.support = Set.range S.u ∪ Set.range S.v

theorem SkewShapes.SkewShape.uv_disjoint (S : SkewShape) : Set.range S.u ∩ Set.range S.v = ∅

noncomputable def SkewShapes.SkewShape.δ (S : SkewShape) (n : ↑S.support) : ↑S.fringe

Equations

• S.δ n = Classical.choose ⋯

@[simp]

theorem SkewShapes.SkewShape.δ_spec (S : SkewShape) (n : ↑S.support) : Δ ↑(S.δ n) = ↑n

theorem SkewShapes.SkewShape.δ_unique (S : SkewShape) (n : ↑S.support) (x : ↑S.fringe) : Δ ↑x = ↑n → x = S.δ n

theorem SkewShapes.SkewShape.u_eq_u_iff (S : SkewShape) (x y : ↥S) : S.u y = S.u x ↔ (↑y).2 = (↑x).2

Two boxes have the same $u$ exactly when they lie in the same column.

theorem SkewShapes.SkewShape.v_eq_v_iff (S : SkewShape) (x y : ↥S) : S.v y = S.v x ↔ (↑y).1 = (↑x).1

Two boxes have the same $v$ exactly when they lie in the same row.

theorem SkewShapes.SkewShape.v_injOn_col (S : SkewShape) (x : ↥S) : Set.InjOn S.v (S.col x)

Distinct boxes in the same column have distinct $v$.

theorem SkewShapes.SkewShape.u_injOn_row (S : SkewShape) (x : ↥S) : Set.InjOn S.u (S.row x)

Distinct boxes in the same row have distinct $u$.

theorem SkewShapes.SkewShape.eq_of_u_eq_of_v_eq (S : SkewShape) {x y : ↥S} (hu : S.u x = S.u y) (hv : S.v x = S.v y) : x = y

A box of $S$ is determined by its pair $(u(x), v(x))$.

theorem SkewShapes.SkewShape.u_mono (S : SkewShape) {x y : ↥S} (h : (↑x).2 ≤ (↑y).2) : S.u x ≤ S.u y

The function $u$ is weakly increasing from west to east.

theorem SkewShapes.SkewShape.v_anti (S : SkewShape) {x y : ↥S} (h : (↑x).1 ≤ (↑y).1) : S.v y ≤ S.v x

The function $v$ is weakly decreasing from north to south.

theorem SkewShapes.SkewShape.pair_injective (S : SkewShape) : Function.Injective S.pair

theorem SkewShapes.SkewShape.u_le_u_iff (S : SkewShape) (x y : ↥S) : S.u x ≤ S.u y ↔ (↑x).2 ≤ (↑y).2

The function $u$ is strictly increasing from west to east.

theorem SkewShapes.SkewShape.v_le_v_iff (S : SkewShape) (x y : ↥S) : S.v x ≤ S.v y ↔ (↑y).1 ≤ (↑x).1

The function $v$ is strictly decreasing from north to south.

theorem SkewShapes.SkewShape.pair_prec_iff (S : SkewShape) (x y : ↥S) : S.pair x ≼ S.pair y ↔ ↑y ≤ ↑x

The interval of $x$ lies inside the interval of $y$ exactly when $y$ is weakly northwest of $x$.

theorem SkewShapes.SkewShape.I_out_u (S : SkewShape) (x : ↥S) : {w : ℤ | (S.u x, w) ∈ S.I} = S.v '' S.col x

The pairs in $I$ starting at $u(x)$ are indexed by the column of $x$.

theorem SkewShapes.SkewShape.I_in_v (S : SkewShape) (x : ↥S) : {w : ℤ | (w, S.v x) ∈ S.I} = S.u '' S.row x

The pairs in $I$ ending at $v(x)$ are indexed by the row of $x$.

theorem SkewShapes.SkewShape.I_in_u (S : SkewShape) (x : ↥S) : {w : ℤ | (w, S.u x) ∈ S.I} = ∅

No pair in $I$ ends at $u(x)$, since $u(x)$ is not a value of $v$.

theorem SkewShapes.SkewShape.I_out_v (S : SkewShape) (x : ↥S) : {w : ℤ | (S.v x, w) ∈ S.I} = ∅

No pair in $I$ starts at $v(x)$, since $v(x)$ is not a value of $u$.

theorem SkewShapes.SkewShape.I_tfree (S : SkewShape) (u w v : ℤ) : (u, w) ∉ S.I ∨ (w, v) ∉ S.I

The set $I$ contains no chain $(u,w), (w,v)$.

theorem SkewShapes.SkewShape.I_aspset_prop (S : SkewShape) : AspSet_prop S.I

def SkewShapes.SkewShape.I_asp (S : SkewShape) : AspSet

Equations

• S.I_asp = { I := S.I, prop := ⋯ }

noncomputable def SkewShapes.SkewShape.σ (S : SkewShape) : AspPerm

The shift-zero permutation associated to a skew shape S.

Equations

• S.σ = S.I_asp.toAspPerm 0

theorem SkewShapes.SkewShape.σ_321a (S : SkewShape) : is_321a S.σ.func

theorem SkewShapes.SkewShape.σ_invSet (S : SkewShape) : inv_set S.σ.func = S.I

theorem SkewShapes.SkewShape.σ_shift (S : SkewShape) : S.σ.χ = 0

theorem SkewShapes.SkewShape.σ_eq (S : SkewShape) (n : ℤ) : S.σ.func n = n + ↑{v : ℤ | (n, v) ∈ S.I}.ncard - ↑{u : ℤ | (u, n) ∈ S.I}.ncard

The reconstruction formula for $\sigma$, which has shift $0$.

theorem SkewShapes.SkewShape.σ_of_u (S : SkewShape) (x : ↥S) : S.σ.func (S.u x) = S.v' x

theorem SkewShapes.SkewShape.σ_of_v (S : SkewShape) (x : ↥S) : S.σ.func (S.v x) = S.u' x

theorem SkewShapes.SkewShape.σ_fixes (S : SkewShape) {n : ℤ} (hn : n ∉ S.support) : S.σ.func n = n

Integers outside the support of $S$ are fixed by $\sigma$.

theorem SkewShapes.SkewShape.σ_inverse_invset (S : SkewShape) : inv_set S.σ.inv.func = S.I'

theorem SkewShapes.SkewShape.u'_eq_flip_u (S : SkewShape) (x : ↥S) : S.u' x = S.flip.u (S.flipBox x)

Reflecting $S$ exchanges $I(S)$ and $I'(S)$.

theorem SkewShapes.SkewShape.v'_eq_flip_v (S : SkewShape) (x : ↥S) : S.v' x = S.flip.v (S.flipBox x)

theorem SkewShapes.SkewShape.I'_eq_flip_I (S : SkewShape) : S.I' = S.flip.I

theorem SkewShapes.SkewShape.flip_σ (S : SkewShape) : S.flip.σ = S.σ⁻¹

The permutation of the reflected shape is the inverse permutation.

theorem SkewShapes.SkewShape.inv_up_closed (S : SkewShape) {τ : AspPerm} (hle : τ ≤L S.σ) {x y : ↥S} (hxy : ↑x ≤ ↑y) (hx : (S.u x, S.v x) ∈ inv_set τ.func) : (S.u y, S.v y) ∈ inv_set τ.func

If $\operatorname{Inv}(\tau) \subseteq I(S)$, then the boxes of $S$ whose pairs lie in $\operatorname{Inv}(\tau)$ are closed to the southeast.

def SkewShapes.SkewShape.restrict (S : SkewShape) (P : ↥S → Prop) (hP : ∀ (x y : ↥S), ↑x ≤ ↑y → P x → P y) : SkewShape

The boxes of $S$ satisfying a predicate closed to the southeast form a skew shape.

Equations

• S.restrict P hP = { boxes := Subtype.val '' {x : ↥S | P x}, closed := ⋯, finite_below := ⋯, finite_above := ⋯ }

theorem SkewShapes.SkewShape.mem_restrict (S : SkewShape) {P : ↥S → Prop} {hP : ∀ (x y : ↥S), ↑x ≤ ↑y → P x → P y} (x : ↥S) : ↑x ∈ S.restrict P hP ↔ P x

theorem SkewShapes.SkewShape.σ_eq_id_of_boxes_eq_empty (S : SkewShape) (h : S.boxes = ∅) : S.σ = AspPerm.id

theorem SkewShapes.SkewShape.boxes_eq_empty_of_σ_eq_id (S : SkewShape) (h : S.σ = AspPerm.id) : S.boxes = ∅