rowLen_anti — Mathlib

English

If i1 ≤ i2, then μ.rowLen(i2) ≤ μ.rowLen(i1).

Русский

Если i1 ≤ i2, то μ.rowLen(i2) ≤ μ.rowLen(i1).

LaTeX

$$$$ \forall \mu,i_1,i_2 \,(i_1 \le i_2) \Rightarrow \mu.rowLen(i_2) \le \mu.rowLen(i_1). $$$$

Lean4

@[mono]
theorem rowLen_anti (μ : YoungDiagram) (i1 i2 : ℕ) (hi : i1 ≤ i2) : μ.rowLen i2 ≤ μ.rowLen i1 :=
  by
  by_contra! h_lt
  rw [← lt_self_iff_false (μ.rowLen i1)]
  rw [← mem_iff_lt_rowLen] at h_lt ⊢
  exact μ.up_left_mem hi (by rfl) h_lt

Похожие утверждения