exists_covBy_of_wellFoundedLT — Mathlib

English

If α is a preorder with a Well-Founded LT (lt), and a is not maximal, there exists a', such that a CovBy a'.

Русский

Если существует WellFounded LT на α и a не максимален, то существует a', для которого a CovBy a'.

LaTeX

$$[wf : WellFoundedLT α] ⟨¬IsMax a⟩ → ∃ a', CovBy a a'$$

Lean4

theorem exists_covBy_of_wellFoundedLT [wf : WellFoundedLT α] ⦃a : α⦄ (h : ¬IsMax a) : ∃ a', a ⋖ a' :=
  by
  rw [not_isMax_iff] at h
  exact ⟨_, wellFounded_lt.min_mem _ h, fun a' ↦ wf.wf.not_lt_min _ h⟩

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