English
If range (c.emb i) = { j }, then c.partSize i = 1.
Русский
Если диапазон (c.emb i) равен { j }, то c.partSize i = 1.
LaTeX
$$$\\operatorname{range}(\\mathrm{emb}\\, i) = \\{ j \\} \\Rightarrow c.partSize(i) = 1$$$
Lean4
/-- If the left-most part is not `{0}`, then the part containing `0` has at least two elements:
either because it's the left-most part, and then it's not just `0` by assumption, or because it's
not the left-most part and then, by increasingness of maximal elements in parts, it contains
a positive element. -/
theorem one_lt_partSize_index_zero (c : OrderedFinpartition (n + 1)) (hc : range (c.emb 0) ≠ {0}) :
1 < c.partSize (c.index 0) :=
by
have : c.partSize (c.index 0) = Nat.card (range (c.emb (c.index 0))) := by
rw [Nat.card_range_of_injective (c.emb_strictMono _).injective]; simp
rw [this]
rcases eq_or_ne (c.index 0) 0 with h | h
· rw [← h] at hc
have : {0} ⊂ range (c.emb (c.index 0)) :=
by
apply ssubset_of_subset_of_ne ?_ hc.symm
simpa only [singleton_subset_iff, mem_range] using ⟨0, emb_zero c⟩
simpa using Set.Finite.card_lt_card (finite_range _) this
· apply one_lt_two.trans_le
have :
{c.emb (c.index 0) 0, c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1, Nat.sub_one_lt_of_lt (c.partSize_pos _)⟩} ⊆
range (c.emb (c.index 0)) :=
by simp [insert_subset]
simp only [emb_zero] at this
convert Nat.card_mono Subtype.finite this
simp only [Nat.card_eq_fintype_card, Fintype.card_ofFinset, toFinset_singleton]
apply (Finset.card_pair ?_).symm
exact ((Fin.zero_le _).trans_lt (c.parts_strictMono ((pos_iff_ne_zero' (c.index 0)).mpr h))).ne
