mem_col_iff — Mathlib

English

For any μ and j and cell c, c is in μ.col(j) iff c is in μ and the second coordinate of c equals j.

Русский

Для любой μ и j и клетки c верно: c ∈ μ.col(j) тогда и только если c ∈ μ и вторая координата c равна j.

LaTeX

$$$$ c \in \mu.col(j) \iff c \in \mu \land \operatorname{snd}(c) = j. $$$$

Lean4

theorem mem_col_iff {μ : YoungDiagram} {j : ℕ} {c : ℕ × ℕ} : c ∈ μ.col j ↔ c ∈ μ ∧ c.snd = j := by simp [col]

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