ext t
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
⊢ ∂ (initSeg s) = initSeg (s.erase (s.min' hs))
case a
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ t ∈ ∂ (initSeg s) ↔ t ∈ initSeg (s.erase (s.min' hs))