exists_notMem_row — Mathlib

English

For any μ and i, there exists a j such that (i,j) ∉ μ.

Русский

Для любой μ и i существует j, такой что (i,j) ∉ μ.

LaTeX

$$$ \forall μ:\text{YoungDiagram},\; \forall i:\mathbb{N},\; \exists j:\mathbb{N},\; (i,j) \notin μ. $$$

Lean4

protected theorem exists_notMem_row (μ : YoungDiagram) (i : ℕ) : ∃ j, (i, j) ∉ μ :=
  by
  obtain ⟨j, hj⟩ :=
    Infinite.exists_notMem_finset
      (μ.cells.preimage (Prod.mk i) fun _ _ _ _ h => by
        cases h
        rfl)
  rw [Finset.mem_preimage] at hj
  exact ⟨j, hj⟩

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