exists_covBy_of_wellFoundedGT — Mathlib

English

If α has Well-Founded GT and a is not minimal, there exists a', such that a' CovBy a.

Русский

Для GT с Well-founded α, если a не минимален, существует a' с a' CovBy a.

LaTeX

$$[wf : WellFoundedGT α] ⟨¬IsMin a⟩ → ∃ a' CovBy a' a$$

Lean4

theorem exists_covBy_of_wellFoundedGT [wf : WellFoundedGT α] ⦃a : α⦄ (h : ¬IsMin a) : ∃ a', a' ⋖ a :=
  by
  rw [not_isMin_iff] at h
  exact ⟨_, wf.wf.min_mem _ h, fun a' h₁ h₂ ↦ wf.wf.not_lt_min _ h h₂ h₁⟩

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