English
If 𝒜 is an initial segment, and 𝒜 is nonempty, then there exists a finite set s with |s|=r such that 𝒜 = initSeg s.
Русский
Если 𝒜 является начальн. сегментом и непусто, существует множество s с |s|=r, такое что 𝒜 = initSeg s.
LaTeX
$$$\exists s.\; |s|=r \land 𝒜 = initSeg(s)$$$
Lean4
theorem exists_initSeg (h𝒜 : IsInitSeg 𝒜 r) (h𝒜₀ : 𝒜.Nonempty) : ∃ s : Finset α, #s = r ∧ 𝒜 = initSeg s :=
by
have hs := sup'_mem (ofColex ⁻¹' 𝒜) (LinearOrder.supClosed _) 𝒜 h𝒜₀ toColex (fun a ha ↦ by simpa using ha)
refine ⟨_, h𝒜.1 hs, ?_⟩
ext t
rw [mem_initSeg]
refine ⟨fun p ↦ ?_, ?_⟩
· rw [h𝒜.1 p, h𝒜.1 hs]
exact ⟨rfl, le_sup' _ p⟩
rintro ⟨cards, le⟩
obtain p | p := le.eq_or_lt
· rwa [toColex_inj.1 p]
· exact h𝒜.2 hs ⟨p, cards ▸ h𝒜.1 hs⟩
