mem_iff_lt_rowLen — Mathlib

English

For every μ and indices i, j, the cell (i,j) belongs to μ if and only if j is less than μ.rowLen(i).

Русский

Для диаграммы Юнга μ и чисел i, j верно: клетка (i,j) принадлежит μ тогда и только если j < μ.rowLen(i).

LaTeX

$$$$ (i,j) \in \mu \iff j < \mu.rowLen(i). $$$$

Lean4

theorem mem_iff_lt_rowLen {μ : YoungDiagram} {i j : ℕ} : (i, j) ∈ μ ↔ j < μ.rowLen i :=
  by
  rw [rowLen, Nat.lt_find_iff]
  push_neg
  exact ⟨fun h _ hmj => μ.up_left_mem (by rfl) hmj h, fun h => h _ (by rfl)⟩

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