superChain_succChain — Mathlib

English

If s is a chain and s is not maximal, then the successor chain is a superchain of s.

Русский

Если s является цепью и не является максимальной, тоSuccChain r s является надцепью по отношению к s.

LaTeX

$$$\\\\forall \\\\alpha \\\\ r \\\\ s, IsChain \\\\ r \\\\ s \\\\land \\\\ neg IsMaxChain \\\\ r \\\\ s \\\\rightarrow SuperChain \\\\ r \\\\ s \\\\ (SuccChain \\\\ r \\\\ s)$$$

Lean4

theorem superChain_succChain (hs₁ : IsChain r s) (hs₂ : ¬IsMaxChain r s) : SuperChain r s (SuccChain r s) :=
  by
  simp only [IsMaxChain, _root_.not_and, not_forall, exists_prop] at hs₂
  obtain ⟨t, ht, hst⟩ := hs₂ hs₁
  exact succChain_spec ⟨t, hs₁, ht, ssubset_iff_subset_ne.2 hst⟩

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