Mathlib Map

Theorems · Theorem · order theory

exists_maximalFor_of_wellFoundedGT

∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder α] [WellFoundedGT α] (P : ι → Prop) (f : ι → α),
  (∃ i, P i) → ∃ i, MaximalFor P f i
Defined in
Mathlib.Order.Minimal
Cited by
2 results in Mathlib
Foundations
Depth 16 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
PreorderWellFoundedGT
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

exists_maximal_of_wellFoundedGT · cited by 1exists_maximal_of_wellFou…WeierstrassCurve.exists_isMinimal · cited by 0WeierstrassCurve.exists_i…Preorder · cited by 7952PreorderWellFoundedGT · cited by 114WellFoundedGTIsWellFounded.wf · cited by 43IsWellFounded.wfWellFounded.has_min · cited by 26WellFounded.has_minMaximalFor · cited by 25MaximalFornot_lt_iff_le_imp_ge · cited by 6not_lt_iff_le_imp_geexists_maximalFor_of_wellFoun…CITED BYCITES

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.