exists_maximalFor_of_wellFoundedGT

English

Under well-founded GT, for any P and f with some P i, there exists i such that MaximalFor P f i.

Русский

При хорошо основанном GT существует i, такое что MaximalFor P f i.

LaTeX

$$$ \exists i, P i \rightarrow \exists i, \operatorname{MaximalFor} P f i $$$

Lean4

theorem exists_maximalFor_of_wellFoundedGT (P : ι → Prop) (f : ι → α) (hP : ∃ i, P i) : ∃ i, MaximalFor P f i :=
  exists_minimalFor_of_wellFoundedLT (α := αᵒᵈ) P f hP

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