English
If chain closures satisfy succ-closure, then a chain closure c1 is contained in c2 whenever c2 is closed under succ and c1 ⊆ c2; the result follows by induction on the structure of ChainClosure.
Русский
Если цепочные оболочки удовлетворяют succ-свойству, то c1 содержится в c2 при условии, что c2 замкну под Succ; доказательство по индукции по структуре ChainClosure.
LaTeX
$$$ \text{ChainClosure}\, r\ c_1 \to \text{ChainClosure}\, r\ c_2 \to (\text{SuccChain } r\ c_2 = c_2) \Rightarrow c_1 \subseteq c_2 $$$
Lean4
theorem succ_fixpoint (hc₁ : ChainClosure r c₁) (hc₂ : ChainClosure r c₂) (hc : SuccChain r c₂ = c₂) : c₁ ⊆ c₂ := by
induction hc₁ with
| succ hc₁ h => exact (chainClosure_succ_total hc₁ hc₂ h).elim (fun h => h ▸ hc.subset) id
| union _ ih => exact sUnion_subset ih
