succ — Mathlib

English

If s is a chain, then the successor chain of s is again a chain.

Русский

Если s является цепью, то SuccChain r s тоже является цепью.

LaTeX

$$$\\\\forall \\\\alpha \\\\ r \\\\ s, IsChain \\\\ r \\\\ s \\\\rightarrow IsChain \\\\ r \\\\ (SuccChain \\\\ r \\\\ s)$$$

Lean4

theorem succ (hs : IsChain r s) : IsChain r (SuccChain r s) :=
  if h : ∃ t, IsChain r s ∧ SuperChain r s t then (succChain_spec h).1
  else by
    rw [exists_and_left] at h
    simpa [SuccChain, dif_neg, h] using hs

Похожие утверждения