English
A variant of the shadow property showing a simple relation for InitSeg.
Русский
Вариант свойства тени, демонстрирующий простую связь InitSeg.
LaTeX
$$$\text{IsInitSeg}(\partial 𝒜) = \text{IsInitSeg}(𝒜)$ under simple adjustments$$
Lean4
/-- The shadow of an initial segment is also an initial segment. -/
protected theorem shadow [Finite α] (h₁ : IsInitSeg 𝒜 r) : IsInitSeg (∂ 𝒜) (r - 1) :=
by
cases nonempty_fintype α
obtain rfl | hr := Nat.eq_zero_or_pos r
· have : 𝒜 ⊆ {∅} := fun s hs ↦ by rw [mem_singleton, ← Finset.card_eq_zero]; exact h₁.1 hs
have := shadow_monotone this
simp only [subset_empty, le_eq_subset, shadow_singleton_empty] at this
simp [this]
obtain rfl | h𝒜 := 𝒜.eq_empty_or_nonempty
· simp
obtain ⟨s, rfl, rfl⟩ := h₁.exists_initSeg h𝒜
rw [shadow_initSeg (card_pos.1 hr), ← card_erase_of_mem (min'_mem _ _)]
exact isInitSeg_initSeg
