exists_minimalFor_of_wellFoundedLT

English

In a well-founded order LT, for any P: ι → Prop and f: ι → α, if at least one i satisfies P i, there exists i that minimizes P along f.

Русский

В хорошо основанном порядке LT для любого P: ι → Prop и функции f: ι → α, если существует i с P i, то найдется i, минимизирующее P вдоль f.

LaTeX

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

Lean4

theorem exists_minimalFor_of_wellFoundedLT (P : ι → Prop) (f : ι → α) (hP : ∃ i, P i) : ∃ i, MinimalFor P f i := by
  simpa [not_lt_iff_le_imp_ge, InvImage] using (instIsWellFoundedInvImage (· < ·) f).wf.has_min _ hP

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