English
There exists a unique OrderedFinpartition 1.
Русский
Существует уникальное OrderedFinpartition(1).
LaTeX
$$$\\exists! c: \\mathrm{OrderedFinpartition}(1)$$$
Lean4
/-- Extend an ordered partition of `n` entries, by adding a new singleton part to the left. -/
@[simps -fullyApplied length partSize]
def extendLeft (c : OrderedFinpartition n) : OrderedFinpartition (n + 1)
where
length := c.length + 1
partSize := Fin.cons 1 c.partSize
partSize_pos := Fin.cases (by simp) (by simp [c.partSize_pos])
emb := Fin.cases (fun _ ↦ 0) (fun m ↦ Fin.succ ∘ c.emb m)
emb_strictMono := by
refine Fin.cases ?_ (fun i ↦ ?_)
· exact @Subsingleton.strictMono _ _ _ _ (by simp; infer_instance) _
· exact strictMono_succ.comp (c.emb_strictMono i)
parts_strictMono i j
hij := by
induction j using Fin.induction with
| zero => simp at hij
| succ j =>
induction i using Fin.induction with
| zero => simp
| succ i =>
simp only [cons_succ, cases_succ, comp_apply, succ_lt_succ_iff]
exact c.parts_strictMono (by simpa using hij)
disjoint i hi j hj
hij := by
wlog h : j < i generalizing i j
· exact .symm (this j (mem_univ j) i (mem_univ i) hij.symm (lt_of_le_of_ne (le_of_not_gt h) hij))
induction i using Fin.induction with
| zero => simp at h
| succ i =>
induction j using Fin.induction with
| zero =>
simp only [onFun, cases_succ, cases_zero]
apply Set.disjoint_iff_forall_ne.2
simp only [mem_range, comp_apply, exists_prop', cons_zero, ne_eq, and_imp, Nonempty.forall, forall_const,
forall_eq', forall_exists_index, forall_apply_eq_imp_iff]
exact fun _ ↦ succ_ne_zero _
| succ j =>
simp only [onFun, cases_succ]
apply Set.disjoint_iff_forall_ne.2
simp only [mem_range, comp_apply, ne_eq, forall_exists_index, forall_apply_eq_imp_iff, succ_inj]
intro a b
apply c.emb_ne_emb_of_ne (by simpa using hij)
cover := by
refine Fin.cases ?_ (fun i ↦ ?_)
· simp only [mem_range]
exact ⟨0, ⟨0, by simp⟩, by simp⟩
· simp only [mem_range]
exact ⟨Fin.succ (c.index i), Fin.cast (by simp) (c.invEmbedding i), by simp⟩
