Upgrading a killing diagram to a nonempty one

Schur vanishing is upward closed, and the empty diagram is below every diagram, so a killed object is killed at some diagram with at least one cell.

theorem RS.YoungDiagram.eq_bot_of_card_eq_zero {lam : YoungDiagram} (h : lam.card = 0) : lam = ⊥

A diagram with no cells is the empty diagram.

theorem RS.exists_killer_card_ne_zero {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.MonoidalLinear ℂ A] (P : SchurPackage) {X : A} {lam : YoungDiagram} (h : SchurKilled P X lam) : ∃ (mu : YoungDiagram), mu.card ≠ 0 ∧ SchurKilled P X mu

A killed object is killed at a nonempty diagram.