exists_minimal_of_wellFoundedLT — Mathlib

English

In a well-founded LT setting, for any P, if there exists i with P i, then there exists i with MinimalFor P i.

Русский

В условиях хорошо основанного LT для любого P, если существует i с P i, то найдется i с MinimalFor P i.

LaTeX

$$$ (\exists i, P i) \rightarrow \exists i, \operatorname{MinimalFor} P i $$$

Lean4

theorem exists_minimal_of_wellFoundedLT (P : α → Prop) (hP : ∃ a, P a) : ∃ a, Minimal P a :=
  exists_minimalFor_of_wellFoundedLT P id hP

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