partSize_eq_one_of_range_emb_eq_singleton

English

The index function satisfies (c.embed (c.index j) (c.invEmbedding j)) = j.

Русский

Индекс-функция удовлетворяет (c.emb (c.index j) (c.invEmbedding j)) = j.

LaTeX

$$$ c.emb (c.index j) (c.invEmbedding j) = j $$$

Lean4

theorem partSize_eq_one_of_range_emb_eq_singleton (c : OrderedFinpartition n) {i : Fin c.length} {j : Fin n}
    (hc : range (c.emb i) = { j }) : c.partSize i = 1 :=
  by
  have : Fintype.card (range (c.emb i)) = Fintype.card (Fin (c.partSize i)) :=
    card_range_of_injective (c.emb_strictMono i).injective
  simpa [hc] using this.symm

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